Step |
Hyp |
Ref |
Expression |
1 |
|
dvelimf.1 |
|- F/ x ph |
2 |
|
dvelimf.2 |
|- F/ z ps |
3 |
|
dvelimf.3 |
|- ( z = y -> ( ph <-> ps ) ) |
4 |
2 3
|
equsal |
|- ( A. z ( z = y -> ph ) <-> ps ) |
5 |
4
|
bicomi |
|- ( ps <-> A. z ( z = y -> ph ) ) |
6 |
|
nfnae |
|- F/ z -. A. x x = y |
7 |
|
nfeqf |
|- ( ( -. A. x x = z /\ -. A. x x = y ) -> F/ x z = y ) |
8 |
7
|
ancoms |
|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x z = y ) |
9 |
1
|
a1i |
|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ph ) |
10 |
8 9
|
nfimd |
|- ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( z = y -> ph ) ) |
11 |
6 10
|
nfald2 |
|- ( -. A. x x = y -> F/ x A. z ( z = y -> ph ) ) |
12 |
5 11
|
nfxfrd |
|- ( -. A. x x = y -> F/ x ps ) |