| Step |
Hyp |
Ref |
Expression |
| 1 |
|
axrep4v |
|- ( A. w E. y A. z ( ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ ph ) ) ) |
| 2 |
|
df-mo |
|- ( E* z ph <-> E. y A. z ( ph -> z = y ) ) |
| 3 |
2
|
albii |
|- ( A. w E* z ph <-> A. w E. y A. z ( ph -> z = y ) ) |
| 4 |
|
df-rex |
|- ( E. w e. x ph <-> E. w ( w e. x /\ ph ) ) |
| 5 |
4
|
bibi2i |
|- ( ( z e. y <-> E. w e. x ph ) <-> ( z e. y <-> E. w ( w e. x /\ ph ) ) ) |
| 6 |
5
|
albii |
|- ( A. z ( z e. y <-> E. w e. x ph ) <-> A. z ( z e. y <-> E. w ( w e. x /\ ph ) ) ) |
| 7 |
6
|
exbii |
|- ( E. y A. z ( z e. y <-> E. w e. x ph ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ ph ) ) ) |
| 8 |
1 3 7
|
3imtr4i |
|- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) ) |