Theorem eqisf ≪ | index | src | ≫ 

theorem eqisf (F G: set) {x: nat}:
  $ isfun F /\ isfun G ->
    (F == G <-> Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x)) $;
StepHypRefExpression
1 bian1a 
(F == G -> Dom F == Dom G) -> (Dom F == Dom G /\ F == G <-> F == G)
2 dmeq 
F == G -> Dom F == Dom G
3 1, 2 ax_mp 
Dom F == Dom G /\ F == G <-> F == G
4 aneq2a 
(Dom F == Dom G -> (F == G <-> A. x (x e. Dom F -> F @ x = G @ x))) -> (Dom F == Dom G /\ F == G <-> Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x))
5 axext2 
F == G <-> A. x A. y (x, y e. F <-> x, y e. G)
6 eqapp 
A. y (x, y e. F <-> x, y e. G) -> F @ x = G @ x
7 6 a1d 
A. y (x, y e. F <-> x, y e. G) -> x e. Dom F -> F @ x = G @ x
8 7 a1i 
isfun F /\ isfun G /\ Dom F == Dom G -> A. y (x, y e. F <-> x, y e. G) -> x e. Dom F -> F @ x = G @ x
9 isfappb 
isfun F -> (x, y e. F <-> x e. Dom F /\ F @ x = y)
10 an3l 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> isfun F
11 9, 10 syl 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x, y e. F <-> x e. Dom F /\ F @ x = y)
12 isfappb 
isfun G -> (x, y e. G <-> x e. Dom G /\ G @ x = y)
13 anllr 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> isfun G
14 12, 13 syl 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x, y e. G <-> x e. Dom G /\ G @ x = y)
15 aneq2a 
(x e. Dom F -> (F @ x = y <-> G @ x = y)) -> (x e. Dom F /\ F @ x = y <-> x e. Dom F /\ G @ x = y)
16 eqeq1 
F @ x = G @ x -> (F @ x = y <-> G @ x = y)
17 anr 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> x e. Dom F -> F @ x = G @ x
18 16, 17 syl6 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> x e. Dom F -> (F @ x = y <-> G @ x = y)
19 15, 18 syl 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x e. Dom F /\ F @ x = y <-> x e. Dom F /\ G @ x = y)
20 anlr 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> Dom F == Dom G
21 20 eleq2d 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x e. Dom F <-> x e. Dom G)
22 21 aneq1d 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x e. Dom F /\ G @ x = y <-> x e. Dom G /\ G @ x = y)
23 19, 22 bitrd 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x e. Dom F /\ F @ x = y <-> x e. Dom G /\ G @ x = y)
24 14, 23 bitr4d 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x, y e. G <-> x e. Dom F /\ F @ x = y)
25 11, 24 bitr4d 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> (x, y e. F <-> x, y e. G)
26 25 iald 
isfun F /\ isfun G /\ Dom F == Dom G /\ (x e. Dom F -> F @ x = G @ x) -> A. y (x, y e. F <-> x, y e. G)
27 26 exp 
isfun F /\ isfun G /\ Dom F == Dom G -> (x e. Dom F -> F @ x = G @ x) -> A. y (x, y e. F <-> x, y e. G)
28 8, 27 ibid 
isfun F /\ isfun G /\ Dom F == Dom G -> (A. y (x, y e. F <-> x, y e. G) <-> x e. Dom F -> F @ x = G @ x)
29 28 aleqd 
isfun F /\ isfun G /\ Dom F == Dom G -> (A. x A. y (x, y e. F <-> x, y e. G) <-> A. x (x e. Dom F -> F @ x = G @ x))
30 5, 29 syl5bb 
isfun F /\ isfun G /\ Dom F == Dom G -> (F == G <-> A. x (x e. Dom F -> F @ x = G @ x))
31 30 exp 
isfun F /\ isfun G -> Dom F == Dom G -> (F == G <-> A. x (x e. Dom F -> F @ x = G @ x))
32 4, 31 syl 
isfun F /\ isfun G -> (Dom F == Dom G /\ F == G <-> Dom F == Dom G /\ A. x (x e. Dom F -> F @ x = G @ x))
33 3, 32 syl5bbr 
isfun F /\ isfun G -> (F == G <-> Dom F == Dom G /\ A. x (x e. Dom F -> 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)