theorem cbvsbh {x y: nat} (a: nat) (p q: wff x y):
$ F/ y p $ >
$ F/ x q $ >
$ x = y -> (p <-> q) $ >
$ [a / x] p <-> [a / y] q $;
Step | Hyp | Ref | Expression |
1 |
|
nfv |
F/ y x = z |
2 |
|
hyp h1 |
F/ y p |
3 |
1, 2 |
nfim |
F/ y x = z -> p |
4 |
|
nfv |
F/ x y = z |
5 |
|
hyp h2 |
F/ x q |
6 |
4, 5 |
nfim |
F/ x y = z -> q |
7 |
|
eqeq1 |
x = y -> (x = z <-> y = z) |
8 |
|
hyp e |
x = y -> (p <-> q) |
9 |
7, 8 |
imeqd |
x = y -> (x = z -> p <-> y = z -> q) |
10 |
3, 6, 9 |
cbvalh |
A. x (x = z -> p) <-> A. y (y = z -> q) |
11 |
10 |
imeq2i |
z = a -> A. x (x = z -> p) <-> z = a -> A. y (y = z -> q) |
12 |
11 |
aleqi |
A. z (z = a -> A. x (x = z -> p)) <-> A. z (z = a -> A. y (y = z -> q)) |
13 |
12 |
conv sb |
[a / x] p <-> [a / y] q |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4,
ax_5,
ax_6,
ax_7,
ax_10,
ax_11,
ax_12)