Axiom ax-pow 1077

Description: Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that the collection of all subsets of a set is also a set. A variant is Axiom Pow of [BellMachover] p. 466 (which can be derived from this version using bm1.3ii 1481). A version using abbreviations is pwex 1806.

Assertion

Ref	Expression
ax-pow	⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Axiom ax-pow

Step	Hyp	Ref	Expression
1		vw	. . . . . . 7 set w
2		vz	. . . . . . 7 set z
3	1, 2	wel 803	. . . . . 6 wff w ∈ z
4		vx	. . . . . . 7 set x
5	1, 4	wel 803	. . . . . 6 wff w ∈ x
6	3, 5	wi 2	. . . . 5 wff (w ∈ z → w ∈ x)
7	6, 1	wal 672	. . . 4 wff ∀w(w ∈ z → w ∈ x)
8		vy	. . . . 5 set y
9	2, 8	wel 803	. . . 4 wff z ∈ y
10	7, 9	wi 2	. . 3 wff (∀w(w ∈ z → w ∈ x) → z ∈ y)
11	10, 2	wal 672	. 2 wff ∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
12	11, 8	wex 678	1 wff ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)

This axiom is referenced by:  axpow 1082

metamath.org