Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002)
Ref | Expression | ||
---|---|---|---|
Assertion | axpowndlem1 | |- ( A. x x = y -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.24 | |- ( x = y -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |
|
2 | 1 | sps | |- ( A. x x = y -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) |