Theorem ssal2 ≪ | index | src | ≫ 

theorem ssal2 (A B: set) {x y: nat}:
  $ A C_ B <-> A. x A. y (x, y e. A -> x, y e. B) $;
StepHypRefExpression
1 bitr 
(A C_ 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 C_ 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 subset 
A C_ 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 C_ 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 imeqd 
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 C_ 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)