Step |
Hyp |
Ref |
Expression |
1 |
|
dtru |
|- -. A. z z = w |
2 |
|
ax-ext |
|- ( A. y ( y e. z <-> y e. w ) -> z = w ) |
3 |
2
|
sps |
|- ( A. w A. y ( y e. z <-> y e. w ) -> z = w ) |
4 |
3
|
alimi |
|- ( A. z A. w A. y ( y e. z <-> y e. w ) -> A. z z = w ) |
5 |
1 4
|
mto |
|- -. A. z A. w A. y ( y e. z <-> y e. w ) |
6 |
|
df-nfc |
|- ( F/_ x x <-> A. y F/ x y e. x ) |
7 |
|
sbnf2 |
|- ( F/ x y e. x <-> A. z A. w ( [ z / x ] y e. x <-> [ w / x ] y e. x ) ) |
8 |
|
elsb4 |
|- ( [ z / x ] y e. x <-> y e. z ) |
9 |
|
elsb4 |
|- ( [ w / x ] y e. x <-> y e. w ) |
10 |
8 9
|
bibi12i |
|- ( ( [ z / x ] y e. x <-> [ w / x ] y e. x ) <-> ( y e. z <-> y e. w ) ) |
11 |
10
|
2albii |
|- ( A. z A. w ( [ z / x ] y e. x <-> [ w / x ] y e. x ) <-> A. z A. w ( y e. z <-> y e. w ) ) |
12 |
7 11
|
bitri |
|- ( F/ x y e. x <-> A. z A. w ( y e. z <-> y e. w ) ) |
13 |
12
|
albii |
|- ( A. y F/ x y e. x <-> A. y A. z A. w ( y e. z <-> y e. w ) ) |
14 |
|
alrot3 |
|- ( A. y A. z A. w ( y e. z <-> y e. w ) <-> A. z A. w A. y ( y e. z <-> y e. w ) ) |
15 |
6 13 14
|
3bitri |
|- ( F/_ x x <-> A. z A. w A. y ( y e. z <-> y e. w ) ) |
16 |
5 15
|
mtbir |
|- -. F/_ x x |