Theorem dfsb2 ≪ | index | src | ≫ 

theorem dfsb2 {x: nat} (a: nat) (b: wff x): $ [a / x] b <-> A. x (x = a -> b) $;
StepHypRefExpression
1 ax_6 
E. y y = a
2 nfal1 
F/ y A. y (y = a -> A. x (x = y -> b))
3 nfv 
F/ y A. x (x = a -> b)
4 eqtr4 
x = a -> y = a -> x = y
5 4 com12 
y = a -> x = a -> x = y
6 5 imim1d 
y = a -> (x = y -> b) -> x = a -> b
7 6 alimd 
y = a -> A. x (x = y -> b) -> A. x (x = a -> b)
8 7 a2i 
(y = a -> A. x (x = y -> b)) -> y = a -> A. x (x = a -> b)
9 eal 
A. y (y = a -> A. x (x = y -> b)) -> y = a -> A. x (x = y -> b)
10 8, 9 syl 
A. y (y = a -> A. x (x = y -> b)) -> y = a -> A. x (x = a -> b)
11 2, 3, 10 eexdh 
A. y (y = a -> A. x (x = y -> b)) -> E. y y = a -> A. x (x = a -> b)
12 1, 11 mpi 
A. y (y = a -> A. x (x = y -> b)) -> A. x (x = a -> b)
13 eqtr 
x = y -> y = a -> x = a
14 13 com12 
y = a -> x = y -> x = a
15 14 imim1d 
y = a -> (x = a -> b) -> x = y -> b
16 15 alimd 
y = a -> A. x (x = a -> b) -> A. x (x = y -> b)
17 16 com12 
A. x (x = a -> b) -> y = a -> A. x (x = y -> b)
18 17 iald 
A. x (x = a -> b) -> A. y (y = a -> A. x (x = y -> b))
19 12, 18 ibii 
A. y (y = a -> A. x (x = y -> b)) <-> A. x (x = a -> b)
20 19 conv sb 
[a / x] b <-> A. x (x = a -> 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_12)