Theorem ssabed ≪ | index | src | ≫ 

theorem ssabed (G: wff) {x: nat} (a: nat) (p: wff x) (q: wff):
  $ G /\ x = a -> p -> q $ >
  $ G -> a e. {x | p} -> q $;
StepHypRefExpression
1 elab2 
a e. {x | p} <-> [a / x] p
2 ax_6 
E. x x = a
3 nfv 
F/ x G
4 nfsb1 
F/ x [a / x] p
5 nfv 
F/ x q
6 4, 5 nfim 
F/ x [a / x] p -> q
7 sbq 
x = a -> (p <-> [a / x] p)
8 7 anwr 
G /\ x = a -> (p <-> [a / x] p)
9 8 bi2d 
G /\ x = a -> [a / x] p -> p
10 hyp h 
G /\ x = a -> p -> q
11 9, 10 syld 
G /\ x = a -> [a / x] p -> q
12 11 exp 
G -> x = a -> [a / x] p -> q
13 3, 6, 12 eexdh 
G -> E. x x = a -> [a / x] p -> q
14 2, 13 mpi 
G -> [a / x] p -> q
15 1, 14 syl5bi 
G -> a e. {x | p} -> q

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)