Theorem sabss ≪ | index | src | ≫ 

theorem sabss {x: nat} (A B: set x): $ S\ x, A C_ S\ x, B <-> A. x A C_ B $;
StepHypRefExpression
1 bitr3 
(A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) <-> S\ x, A C_ S\ x, B) ->
  (A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) <-> A. x A C_ B) ->
  (S\ x, A C_ S\ x, B <-> A. x A C_ B)
2 ssab 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) <-> {a2 | snd a2 e. S[fst a2 / x] A} C_ {a2 | snd a2 e. S[fst a2 / x] B}
3 2 conv sab 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) <-> S\ x, A C_ S\ x, B
4 1, 3 ax_mp 
(A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) <-> A. x A C_ B) -> (S\ x, A C_ S\ x, B <-> A. x A C_ B)
5 nfsbs1 
FS/ x S[fst a2 / x] A
6 5 nfel2 
F/ x snd a2 e. S[fst a2 / x] A
7 nfsbs1 
FS/ x S[fst a2 / x] B
8 7 nfel2 
F/ x snd a2 e. S[fst a2 / x] B
9 6, 8 nfim 
F/ x snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B
10 9 nfal 
F/ x A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B)
11 sndpr 
snd (x, a1) = a1
12 sndeq 
a2 = x, a1 -> snd a2 = snd (x, a1)
13 11, 12 syl6eq 
a2 = x, a1 -> snd a2 = a1
14 sbsq 
x = fst a2 -> A == S[fst a2 / x] A
15 fstpr 
fst (x, a1) = x
16 fsteq 
a2 = x, a1 -> fst a2 = fst (x, a1)
17 15, 16 syl6eq 
a2 = x, a1 -> fst a2 = x
18 17 eqcomd 
a2 = x, a1 -> x = fst a2
19 14, 18 syl 
a2 = x, a1 -> A == S[fst a2 / x] A
20 19 eqscomd 
a2 = x, a1 -> S[fst a2 / x] A == A
21 13, 20 eleqd 
a2 = x, a1 -> (snd a2 e. S[fst a2 / x] A <-> a1 e. A)
22 sbsq 
x = fst a2 -> B == S[fst a2 / x] B
23 22, 18 syl 
a2 = x, a1 -> B == S[fst a2 / x] B
24 23 eqscomd 
a2 = x, a1 -> S[fst a2 / x] B == B
25 13, 24 eleqd 
a2 = x, a1 -> (snd a2 e. S[fst a2 / x] B <-> a1 e. B)
26 21, 25 imeqd 
a2 = x, a1 -> (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B <-> a1 e. A -> a1 e. B)
27 26 eale 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) -> a1 e. A -> a1 e. B
28 27 iald 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) -> A. a1 (a1 e. A -> a1 e. B)
29 28 conv subset 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) -> A C_ B
30 10, 29 ialdh 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) -> A. x A C_ B
31 ssel 
S[fst a2 / x] A C_ S[fst a2 / x] B -> snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B
32 5, 7 nfss 
F/ x S[fst a2 / x] A C_ S[fst a2 / x] B
33 14, 22 sseqd 
x = fst a2 -> (A C_ B <-> S[fst a2 / x] A C_ S[fst a2 / x] B)
34 32, 33 ealeh 
A. x A C_ B -> S[fst a2 / x] A C_ S[fst a2 / x] B
35 31, 34 syl 
A. x A C_ B -> snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B
36 35 iald 
A. x A C_ B -> A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B)
37 30, 36 ibii 
A. a2 (snd a2 e. S[fst a2 / x] A -> snd a2 e. S[fst a2 / x] B) <-> A. x A C_ B
38 4, 37 ax_mp 
S\ x, A C_ S\ x, B <-> A. x A C_ 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)