Axiom ax-pow 2818

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. the collection of all subsets of x. The variant axpow2 2820 states that the power set itself exists. A version using class notation is pwex 2823.

Assertion

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

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-pow

Step	Hyp	Ref	Expression
1		vw	. . . . . . . 8 set w
2	1	cv 991	. . . . . . 7 class w
3		vz	. . . . . . . 8 set z
4	3	cv 991	. . . . . . 7 class z
5	2, 4	wcel 994	. . . . . 6 wff w ∈ z
6		vx	. . . . . . . 8 set x
7	6	cv 991	. . . . . . 7 class x
8	2, 7	wcel 994	. . . . . 6 wff w ∈ x
9	5, 8	wi 3	. . . . 5 wff (w ∈ z → w ∈ x)
10	9, 1	wal 990	. . . 4 wff ∀w(w ∈ z → w ∈ x)
11		vy	. . . . . 6 set y
12	11	cv 991	. . . . 5 class y
13	4, 12	wcel 994	. . . 4 wff z ∈ y
14	10, 13	wi 3	. . 3 wff (∀w(w ∈ z → w ∈ x) → z ∈ y)
15	14, 3	wal 990	. 2 wff ∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
16	15, 11	wex 1016	1 wff ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)

This axiom is referenced by:  zfpow 2819  axpow2 2820  el 2822  dtru 2831

Copyright terms: Public domain