Description: Power set axiom: the powerclass of a set is a set. Axiom 4 of TakeutiZaring p. 17. (Contributed by NM, 30-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011) Revised to prove pwexg from vpwex . (Revised by BJ, 10-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | vpwex | |- ~P x e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pw | |- ~P x = { w | w C_ x } |
|
| 2 | axpow2 | |- E. y A. z ( z C_ x -> z e. y ) |
|
| 3 | 2 | sepexi | |- E. y A. z ( z e. y <-> z C_ x ) |
| 4 | sseq1 | |- ( w = z -> ( w C_ x <-> z C_ x ) ) |
|
| 5 | 4 | eqabbw | |- ( y = { w | w C_ x } <-> A. z ( z e. y <-> z C_ x ) ) |
| 6 | 5 | exbii | |- ( E. y y = { w | w C_ x } <-> E. y A. z ( z e. y <-> z C_ x ) ) |
| 7 | 3 6 | mpbir | |- E. y y = { w | w C_ x } |
| 8 | 7 | issetri | |- { w | w C_ x } e. _V |
| 9 | 1 8 | eqeltri | |- ~P x e. _V |