Step |
Hyp |
Ref |
Expression |
1 |
|
ax-pow |
|- E. x A. y ( A. w ( w e. y -> w e. z ) -> y e. x ) |
2 |
|
elequ1 |
|- ( w = x -> ( w e. y <-> x e. y ) ) |
3 |
|
elequ1 |
|- ( w = x -> ( w e. z <-> x e. z ) ) |
4 |
2 3
|
imbi12d |
|- ( w = x -> ( ( w e. y -> w e. z ) <-> ( x e. y -> x e. z ) ) ) |
5 |
4
|
cbvalvw |
|- ( A. w ( w e. y -> w e. z ) <-> A. x ( x e. y -> x e. z ) ) |
6 |
5
|
imbi1i |
|- ( ( A. w ( w e. y -> w e. z ) -> y e. x ) <-> ( A. x ( x e. y -> x e. z ) -> y e. x ) ) |
7 |
6
|
albii |
|- ( A. y ( A. w ( w e. y -> w e. z ) -> y e. x ) <-> A. y ( A. x ( x e. y -> x e. z ) -> y e. x ) ) |
8 |
7
|
exbii |
|- ( E. x A. y ( A. w ( w e. y -> w e. z ) -> y e. x ) <-> E. x A. y ( A. x ( x e. y -> x e. z ) -> y e. x ) ) |
9 |
1 8
|
mpbi |
|- E. x A. y ( A. x ( x e. y -> x e. z ) -> y e. x ) |