# Metamath Proof Explorer

## Axiom ax-pow

Description: Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the power set of a given set x i.e. contains every subset of x . The variant axpow2 uses explicit subset notation. A version using class notation is pwex . (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion ax-pow ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\to {w}\in {x}\right)\to {z}\in {y}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vy ${setvar}{y}$
1 vz ${setvar}{z}$
2 vw ${setvar}{w}$
3 2 cv ${setvar}{w}$
4 1 cv ${setvar}{z}$
5 3 4 wcel ${wff}{w}\in {z}$
6 vx ${setvar}{x}$
7 6 cv ${setvar}{x}$
8 3 7 wcel ${wff}{w}\in {x}$
9 5 8 wi ${wff}\left({w}\in {z}\to {w}\in {x}\right)$
10 9 2 wal ${wff}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\to {w}\in {x}\right)$
11 0 cv ${setvar}{y}$
12 4 11 wcel ${wff}{z}\in {y}$
13 10 12 wi ${wff}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\to {w}\in {x}\right)\to {z}\in {y}\right)$
14 13 1 wal ${wff}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\to {w}\in {x}\right)\to {z}\in {y}\right)$
15 14 0 wex ${wff}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {z}\to {w}\in {x}\right)\to {z}\in {y}\right)$