Step |
Hyp |
Ref |
Expression |
1 |
|
cbvmow.1 |
|- F/ y ph |
2 |
|
cbvmow.2 |
|- F/ x ps |
3 |
|
cbvmow.3 |
|- ( x = y -> ( ph <-> ps ) ) |
4 |
|
nfv |
|- F/ y x = z |
5 |
1 4
|
nfim |
|- F/ y ( ph -> x = z ) |
6 |
|
nfv |
|- F/ x y = z |
7 |
2 6
|
nfim |
|- F/ x ( ps -> y = z ) |
8 |
|
equequ1 |
|- ( x = y -> ( x = z <-> y = z ) ) |
9 |
3 8
|
imbi12d |
|- ( x = y -> ( ( ph -> x = z ) <-> ( ps -> y = z ) ) ) |
10 |
5 7 9
|
cbvalv1 |
|- ( A. x ( ph -> x = z ) <-> A. y ( ps -> y = z ) ) |
11 |
10
|
exbii |
|- ( E. z A. x ( ph -> x = z ) <-> E. z A. y ( ps -> y = z ) ) |
12 |
|
df-mo |
|- ( E* x ph <-> E. z A. x ( ph -> x = z ) ) |
13 |
|
df-mo |
|- ( E* y ps <-> E. z A. y ( ps -> y = z ) ) |
14 |
11 12 13
|
3bitr4i |
|- ( E* x ph <-> E* y ps ) |