| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-wl-11v |
|- ( A. u A. x [ u / y ] ph -> A. x A. u [ u / y ] ph ) |
| 2 |
|
ax-wl-11v |
|- ( A. x A. u [ u / y ] ph -> A. u A. x [ u / y ] ph ) |
| 3 |
1 2
|
impbii |
|- ( A. u A. x [ u / y ] ph <-> A. x A. u [ u / y ] ph ) |
| 4 |
|
nfna1 |
|- F/ x -. A. x x = y |
| 5 |
|
wl-ax11-lem3 |
|- ( -. A. x x = y -> F/ x A. u u = y ) |
| 6 |
4 5
|
nfan1 |
|- F/ x ( -. A. x x = y /\ A. u u = y ) |
| 7 |
|
wl-ax11-lem5 |
|- ( A. u u = y -> ( A. u [ u / y ] ph <-> A. y ph ) ) |
| 8 |
7
|
adantl |
|- ( ( -. A. x x = y /\ A. u u = y ) -> ( A. u [ u / y ] ph <-> A. y ph ) ) |
| 9 |
6 8
|
albid |
|- ( ( -. A. x x = y /\ A. u u = y ) -> ( A. x A. u [ u / y ] ph <-> A. x A. y ph ) ) |
| 10 |
9
|
ancoms |
|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. x A. u [ u / y ] ph <-> A. x A. y ph ) ) |
| 11 |
3 10
|
bitrid |
|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. u A. x [ u / y ] ph <-> A. x A. y ph ) ) |