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

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 ∈ z
6 vx setvar x
7 6 cv setvar x
8 3 7 wcel wff w ∈ x
9 5 8 wi wff w ∈ z → w ∈ x
10 9 2 wal wff ∀ w w ∈ z → w ∈ x
11 0 cv setvar y
12 4 11 wcel wff z ∈ y
13 10 12 wi wff ∀ w w ∈ z → w ∈ x → z ∈ y
14 13 1 wal wff ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
15 14 0 wex wff ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y