Theorem funcal ≪ | index | src | ≫ 

theorem funcal (A B F: set) {x: nat}:
  $ func F A B <-> isfun F /\ Dom F == A /\ A. x (x e. A -> F @ x e. B) $;
StepHypRefExpression
1 aneq2a 
(isfun F /\ Dom F == A -> (Ran F C_ B <-> A. x (x e. A -> F @ x e. B))) ->
  (isfun F /\ Dom F == A /\ Ran F C_ B <-> isfun F /\ Dom F == A /\ A. x (x e. A -> F @ x e. B))
2 1 conv func 
(isfun F /\ Dom F == A -> (Ran F C_ B <-> A. x (x e. A -> F @ x e. B))) -> (func F A B <-> isfun F /\ Dom F == A /\ A. x (x e. A -> F @ x e. B))
3 isfrnss 
isfun F -> (Ran F C_ B <-> A. x (x e. Dom F -> F @ x e. B))
4 3 anwl 
isfun F /\ Dom F == A -> (Ran F C_ B <-> A. x (x e. Dom F -> F @ x e. B))
5 anr 
isfun F /\ Dom F == A -> Dom F == A
6 5 eleq2d 
isfun F /\ Dom F == A -> (x e. Dom F <-> x e. A)
7 6 imeq1d 
isfun F /\ Dom F == A -> (x e. Dom F -> F @ x e. B <-> x e. A -> F @ x e. B)
8 7 aleqd 
isfun F /\ Dom F == A -> (A. x (x e. Dom F -> F @ x e. B) <-> A. x (x e. A -> F @ x e. B))
9 4, 8 bitrd 
isfun F /\ Dom F == A -> (Ran F C_ B <-> A. x (x e. A -> F @ x e. B))
10 2, 9 ax_mp 
func F A B <-> isfun F /\ Dom F == A /\ A. x (x e. A -> F @ x e. B)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano2, addeq, muleq)