Theorem eqfunc ≪ | index | src | ≫ 

theorem eqfunc (A B C F G: set) {x: nat}:
  $ func F A B /\ func G A C -> (F == G <-> A. x (x e. A -> F @ x = G @ x)) $;
StepHypRefExpression
1 anim 
(func F A B -> isfun F) -> (func G A C -> isfun G) -> func F A B /\ func G A C -> isfun F /\ isfun G
2 funcisf 
func F A B -> isfun F
3 1, 2 ax_mp 
(func G A C -> isfun G) -> func F A B /\ func G A C -> isfun F /\ isfun G
4 funcisf 
func G A C -> isfun G
5 3, 4 ax_mp 
func F A B /\ func G A C -> isfun F /\ isfun G
6 eqisf 
isfun F /\ isfun G -> (F == G <-> Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x))
7 5, 6 rsyl 
func F A B /\ func G A C -> (F == G <-> Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x))
8 bian1 
Dom F == Dom G -> (Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x) <-> A. x (x e. Dom F -> F @ x = G @ x))
9 funcdm 
func F A B -> Dom F == A
10 9 anwl 
func F A B /\ func G A C -> Dom F == A
11 funcdm 
func G A C -> Dom G == A
12 11 anwr 
func F A B /\ func G A C -> Dom G == A
13 10, 12 eqstr4d 
func F A B /\ func G A C -> Dom F == Dom G
14 8, 13 syl 
func F A B /\ func G A C -> (Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x) <-> A. x (x e. Dom F -> F @ x = G @ x))
15 10 eleq2d 
func F A B /\ func G A C -> (x e. Dom F <-> x e. A)
16 15 imeq1d 
func F A B /\ func G A C -> (x e. Dom F -> F @ x = G @ x <-> x e. A -> F @ x = G @ x)
17 16 aleqd 
func F A B /\ func G A C -> (A. x (x e. Dom F -> F @ x = G @ x) <-> A. x (x e. A -> F @ x = G @ x))
18 14, 17 bitrd 
func F A B /\ func G A C -> (Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x) <-> A. x (x e. A -> F @ x = G @ x))
19 7, 18 bitrd 
func F A B /\ func G A C -> (F == G <-> A. x (x e. A -> F @ x = G @ x))

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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)