Theorem sbq | index | src |

theorem sbq {x: nat} (a: nat) (b: wff x): $ x = a -> (b <-> [a / x] b) $;
StepHypRefExpression
1 ax_12
x = y -> b -> A. x (x = y -> b)
2 anll
x = a /\ b /\ y = a -> x = a
3 anr
x = a /\ b /\ y = a -> y = a
4 2, 3 eqtr4d
x = a /\ b /\ y = a -> x = y
5 anlr
x = a /\ b /\ y = a -> b
6 1, 4, 5 sylc
x = a /\ b /\ y = a -> A. x (x = y -> b)
7 6 ialda
x = a /\ b -> A. y (y = a -> A. x (x = y -> b))
8 7 exp
x = a -> b -> A. y (y = a -> A. x (x = y -> b))
9 ax_6
E. y y = a
10 nfv
F/ y x = a
11 nfal1
F/ y A. y (y = a -> A. x (x = y -> b))
12 nfv
F/ y b
13 11, 12 nfim
F/ y A. y (y = a -> A. x (x = y -> b)) -> b
14 eal
A. y (y = a -> A. x (x = y -> b)) -> y = a -> A. x (x = y -> b)
15 anr
x = a /\ y = a -> y = a
16 15 imim1i
(y = a -> A. x (x = y -> b)) -> x = a /\ y = a -> A. x (x = y -> b)
17 16 com12
x = a /\ y = a -> (y = a -> A. x (x = y -> b)) -> A. x (x = y -> b)
18 eal
A. x (x = y -> b) -> x = y -> b
19 18 com12
x = y -> A. x (x = y -> b) -> b
20 eqtr4
x = a -> y = a -> x = y
21 20 imp
x = a /\ y = a -> x = y
22 19, 21 syl
x = a /\ y = a -> A. x (x = y -> b) -> b
23 17, 22 syld
x = a /\ y = a -> (y = a -> A. x (x = y -> b)) -> b
24 14, 23 syl5
x = a /\ y = a -> A. y (y = a -> A. x (x = y -> b)) -> b
25 24 exp
x = a -> y = a -> A. y (y = a -> A. x (x = y -> b)) -> b
26 10, 13, 25 eexdh
x = a -> E. y y = a -> A. y (y = a -> A. x (x = y -> b)) -> b
27 9, 26 mpi
x = a -> A. y (y = a -> A. x (x = y -> b)) -> b
28 8, 27 ibid
x = a -> (b <-> A. y (y = a -> A. x (x = y -> b)))
29 28 conv sb
x = a -> (b <-> [a / x] 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)