Theorem axext2 ≪ | index | src | ≫ 

theorem axext2 (A B: set) {x y: nat}:
  $ A == B <-> A. x A. y (x, y e. A <-> x, y e. B) $;
StepHypRefExpression
1 bitr 
(A == B <-> A. p A. x A. y (p = x, y -> (p e. A <-> p e. B))) ->
  (A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B)) ->
  (A == B <-> A. x A. y (x, y e. A <-> x, y e. B))
2 bitr3 
(E. x E. y p = x, y -> (p e. A <-> p e. B) <-> (p e. A <-> p e. B)) ->
  (E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))) ->
  (p e. A <-> p e. B <-> A. x A. y (p = x, y -> (p e. A <-> p e. B)))
3 biim1 
E. x E. y p = x, y -> (E. x E. y p = x, y -> (p e. A <-> p e. B) <-> (p e. A <-> p e. B))
4 expr 
E. x E. y p = x, y
5 3, 4 ax_mp 
E. x E. y p = x, y -> (p e. A <-> p e. B) <-> (p e. A <-> p e. B)
6 2, 5 ax_mp 
(E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))) ->
  (p e. A <-> p e. B <-> A. x A. y (p = x, y -> (p e. A <-> p e. B)))
7 bitr 
(E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x (E. y p = x, y -> (p e. A <-> p e. B))) ->
  (A. x (E. y p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))) ->
  (E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B)))
8 eexb 
E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x (E. y p = x, y -> (p e. A <-> p e. B))
9 7, 8 ax_mp 
(A. x (E. y p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))) ->
  (E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B)))
10 eexb 
E. y p = x, y -> (p e. A <-> p e. B) <-> A. y (p = x, y -> (p e. A <-> p e. B))
11 10 aleqi 
A. x (E. y p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))
12 9, 11 ax_mp 
E. x E. y p = x, y -> (p e. A <-> p e. B) <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))
13 6, 12 ax_mp 
p e. A <-> p e. B <-> A. x A. y (p = x, y -> (p e. A <-> p e. B))
14 13 aleqi 
A. p (p e. A <-> p e. B) <-> A. p A. x A. y (p = x, y -> (p e. A <-> p e. B))
15 14 conv eqs 
A == B <-> A. p A. x A. y (p = x, y -> (p e. A <-> p e. B))
16 1, 15 ax_mp 
(A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B)) -> (A == B <-> A. x A. y (x, y e. A <-> x, y e. B))
17 bitr 
(A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. p A. y (p = x, y -> (p e. A <-> p e. B))) ->
  (A. x A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B)) ->
  (A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B))
18 alcomb 
A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. p A. y (p = x, y -> (p e. A <-> p e. B))
19 17, 18 ax_mp 
(A. x A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B)) ->
  (A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B))
20 bitr 
(A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. y A. p (p = x, y -> (p e. A <-> p e. B))) ->
  (A. y A. p (p = x, y -> (p e. A <-> p e. B)) <-> A. y (x, y e. A <-> x, y e. B)) ->
  (A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. y (x, y e. A <-> x, y e. B))
21 alcomb 
A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. y A. p (p = x, y -> (p e. A <-> p e. B))
22 20, 21 ax_mp 
(A. y A. p (p = x, y -> (p e. A <-> p e. B)) <-> A. y (x, y e. A <-> x, y e. B)) ->
  (A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. y (x, y e. A <-> x, y e. B))
23 eleq1 
p = x, y -> (p e. A <-> x, y e. A)
24 eleq1 
p = x, y -> (p e. B <-> x, y e. B)
25 23, 24 bieqd 
p = x, y -> (p e. A <-> p e. B <-> (x, y e. A <-> x, y e. B))
26 25 aleqe 
A. p (p = x, y -> (p e. A <-> p e. B)) <-> (x, y e. A <-> x, y e. B)
27 26 aleqi 
A. y A. p (p = x, y -> (p e. A <-> p e. B)) <-> A. y (x, y e. A <-> x, y e. B)
28 22, 27 ax_mp 
A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. y (x, y e. A <-> x, y e. B)
29 28 aleqi 
A. x A. p A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B)
30 19, 29 ax_mp 
A. p A. x A. y (p = x, y -> (p e. A <-> p e. B)) <-> A. x A. y (x, y e. A <-> x, y e. B)
31 16, 30 ax_mp 
A == B <-> A. x A. y (x, y e. A <-> x, y 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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)