Theorem xabssd ≪ | index | src | ≫ 

theorem xabssd (A: set) (G: wff) {x: nat} (B C: set x):
  $ G /\ x e. A -> B C_ C $ >
  $ G -> X\ x e. A, B C_ X\ x e. A, C $;
StepHypRefExpression
1 anim2a 
(fst a1 e. A -> snd a1 e. S[fst a1 / x] B -> snd a1 e. S[fst a1 / x] C) -> fst a1 e. A /\ snd a1 e. S[fst a1 / x] B -> fst a1 e. A /\ snd a1 e. S[fst a1 / x] C
2 ssel 
S[fst a1 / x] B C_ S[fst a1 / x] C -> snd a1 e. S[fst a1 / x] B -> snd a1 e. S[fst a1 / x] C
3 nfv 
F/ x G /\ fst a1 e. A
4 nfsbs1 
FS/ x S[fst a1 / x] B
5 nfsbs1 
FS/ x S[fst a1 / x] C
6 4, 5 nfss 
F/ x S[fst a1 / x] B C_ S[fst a1 / x] C
7 3, 6 nfim 
F/ x G /\ fst a1 e. A -> S[fst a1 / x] B C_ S[fst a1 / x] C
8 hyp h 
G /\ x e. A -> B C_ C
9 eleq1 
x = fst a1 -> (x e. A <-> fst a1 e. A)
10 9 aneq2d 
x = fst a1 -> (G /\ x e. A <-> G /\ fst a1 e. A)
11 sbsq 
x = fst a1 -> B == S[fst a1 / x] B
12 sbsq 
x = fst a1 -> C == S[fst a1 / x] C
13 11, 12 sseqd 
x = fst a1 -> (B C_ C <-> S[fst a1 / x] B C_ S[fst a1 / x] C)
14 10, 13 imeqd 
x = fst a1 -> (G /\ x e. A -> B C_ C <-> G /\ fst a1 e. A -> S[fst a1 / x] B C_ S[fst a1 / x] C)
15 7, 8, 14 sbethh 
G /\ fst a1 e. A -> S[fst a1 / x] B C_ S[fst a1 / x] C
16 2, 15 syl 
G /\ fst a1 e. A -> snd a1 e. S[fst a1 / x] B -> snd a1 e. S[fst a1 / x] C
17 16 exp 
G -> fst a1 e. A -> snd a1 e. S[fst a1 / x] B -> snd a1 e. S[fst a1 / x] C
18 1, 17 syl 
G -> fst a1 e. A /\ snd a1 e. S[fst a1 / x] B -> fst a1 e. A /\ snd a1 e. S[fst a1 / x] C
19 18 ssabd 
G -> {a1 | fst a1 e. A /\ snd a1 e. S[fst a1 / x] B} C_ {a1 | fst a1 e. A /\ snd a1 e. S[fst a1 / x] C}
20 19 conv xab 
G -> X\ x e. A, B C_ X\ x e. A, C

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)