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 ⊢∃y∀z∀ww∈z→w∈x→z∈y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy setvary
1 vz setvarz
2 vw setvarw
3 2 cv setvarw
4 1 cv setvarz
5 3 4 wcel wffw∈z
6 vx setvarx
7 6 cv setvarx
8 3 7 wcel wffw∈x
9 5 8 wi wffw∈z→w∈x
10 9 2 wal wff∀ww∈z→w∈x
11 0 cv setvary
12 4 11 wcel wffz∈y
13 10 12 wi wff∀ww∈z→w∈x→z∈y
14 13 1 wal wff∀z∀ww∈z→w∈x→z∈y
15 14 0 wex wff∃y∀z∀ww∈z→w∈x→z∈y