| Step |
Hyp |
Ref |
Expression |
| 1 |
|
axrep6 |
|- ( A. w E* z ( w e. x /\ ph ) -> E. y A. z ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) ) |
| 2 |
|
19.37v |
|- ( E. y ( w e. x -> A. z ( ph -> z = y ) ) <-> ( w e. x -> E. y A. z ( ph -> z = y ) ) ) |
| 3 |
|
impexp |
|- ( ( ( w e. x /\ ph ) -> z = y ) <-> ( w e. x -> ( ph -> z = y ) ) ) |
| 4 |
3
|
albii |
|- ( A. z ( ( w e. x /\ ph ) -> z = y ) <-> A. z ( w e. x -> ( ph -> z = y ) ) ) |
| 5 |
|
19.21v |
|- ( A. z ( w e. x -> ( ph -> z = y ) ) <-> ( w e. x -> A. z ( ph -> z = y ) ) ) |
| 6 |
4 5
|
bitri |
|- ( A. z ( ( w e. x /\ ph ) -> z = y ) <-> ( w e. x -> A. z ( ph -> z = y ) ) ) |
| 7 |
6
|
exbii |
|- ( E. y A. z ( ( w e. x /\ ph ) -> z = y ) <-> E. y ( w e. x -> A. z ( ph -> z = y ) ) ) |
| 8 |
|
dfmo |
|- ( E* z ph <-> E. y A. z ( ph -> z = y ) ) |
| 9 |
8
|
imbi2i |
|- ( ( w e. x -> E* z ph ) <-> ( w e. x -> E. y A. z ( ph -> z = y ) ) ) |
| 10 |
2 7 9
|
3bitr4i |
|- ( E. y A. z ( ( w e. x /\ ph ) -> z = y ) <-> ( w e. x -> E* z ph ) ) |
| 11 |
10
|
albii |
|- ( A. w E. y A. z ( ( w e. x /\ ph ) -> z = y ) <-> A. w ( w e. x -> E* z ph ) ) |
| 12 |
|
dfmo |
|- ( E* z ( w e. x /\ ph ) <-> E. y A. z ( ( w e. x /\ ph ) -> z = y ) ) |
| 13 |
12
|
albii |
|- ( A. w E* z ( w e. x /\ ph ) <-> A. w E. y A. z ( ( w e. x /\ ph ) -> z = y ) ) |
| 14 |
|
df-ral |
|- ( A. w e. x E* z ph <-> A. w ( w e. x -> E* z ph ) ) |
| 15 |
11 13 14
|
3bitr4i |
|- ( A. w E* z ( w e. x /\ ph ) <-> A. w e. x E* z ph ) |
| 16 |
|
rexanid |
|- ( E. w e. x ( w e. x /\ ph ) <-> E. w e. x ph ) |
| 17 |
16
|
bibi2i |
|- ( ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) <-> ( z e. y <-> E. w e. x ph ) ) |
| 18 |
17
|
albii |
|- ( A. z ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) <-> A. z ( z e. y <-> E. w e. x ph ) ) |
| 19 |
18
|
exbii |
|- ( E. y A. z ( z e. y <-> E. w e. x ( w e. x /\ ph ) ) <-> E. y A. z ( z e. y <-> E. w e. x ph ) ) |
| 20 |
1 15 19
|
3imtr3i |
|- ( A. w e. x E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) ) |