theorem sbco {x y: nat} (a: nat x) (b: wff x):
$ [a / y] [y / x] b <-> [a / x] b $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
bitr |
([a / y] [y / x] b <-> A. y (y = a -> [y / x] b)) -> (A. y (y = a -> [y / x] b) <-> [a / x] b) -> ([a / y] [y / x] b <-> [a / x] b) |
| 2 |
|
dfsb2 |
[a / y] [y / x] b <-> A. y (y = a -> [y / x] b) |
| 3 |
1, 2 |
ax_mp |
(A. y (y = a -> [y / x] b) <-> [a / x] b) -> ([a / y] [y / x] b <-> [a / x] b) |
| 4 |
|
dfsb2 |
[y / x] b <-> A. x (x = y -> b) |
| 5 |
4 |
imeq2i |
y = a -> [y / x] b <-> y = a -> A. x (x = y -> b) |
| 6 |
5 |
aleqi |
A. y (y = a -> [y / x] b) <-> A. y (y = a -> A. x (x = y -> b)) |
| 7 |
6 |
conv sb |
A. y (y = a -> [y / x] b) <-> [a / x] b |
| 8 |
3, 7 |
ax_mp |
[a / y] [y / x] 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)