Theorem dfsb3 | index | src |

theorem dfsb3 {x: nat} (a: nat) (b: wff x): $ [a / x] b <-> E. x (x = a /\ b) $;
StepHypRefExpression
1 nfex1
F/ x E. x (x = a /\ b)
2 con2b
(A. x ~(x = a /\ b) <-> ~b) -> (b <-> ~A. x ~(x = a /\ b))
3 2 conv ex
(A. x ~(x = a /\ b) <-> ~b) -> (b <-> E. x (x = a /\ b))
4 bitr4
(A. x ~(x = a /\ b) <-> A. x (x = a -> ~b)) -> ([a / x] ~b <-> A. x (x = a -> ~b)) -> (A. x ~(x = a /\ b) <-> [a / x] ~b)
5 notan2
~(x = a /\ b) <-> x = a -> ~b
6 5 aleqi
A. x ~(x = a /\ b) <-> A. x (x = a -> ~b)
7 4, 6 ax_mp
([a / x] ~b <-> A. x (x = a -> ~b)) -> (A. x ~(x = a /\ b) <-> [a / x] ~b)
8 dfsb2
[a / x] ~b <-> A. x (x = a -> ~b)
9 7, 8 ax_mp
A. x ~(x = a /\ b) <-> [a / x] ~b
10 sbq
x = a -> (~b <-> [a / x] ~b)
11 10 bicomd
x = a -> ([a / x] ~b <-> ~b)
12 9, 11 syl5bb
x = a -> (A. x ~(x = a /\ b) <-> ~b)
13 3, 12 syl
x = a -> (b <-> E. x (x = a /\ b))
14 1, 13 sbeh
[a / x] b <-> E. 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_11, ax_12)