Axiom ax-pow 3649

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 3651 uses explicit subset notation. A version using class notation is pwex 3654.

Assertion

Ref	Expression
ax-pow	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. 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 1585	. . . . . . 7 class w
3		vz	. . . . . . . 8 set z
4	3	cv 1585	. . . . . . 7 class z
5	2, 4	wcel 1588	. . . . . 6 wff w e. z
6		vx	. . . . . . . 8 set x
7	6	cv 1585	. . . . . . 7 class x
8	2, 7	wcel 1588	. . . . . 6 wff w e. x
9	5, 8	wi 3	. . . . 5 wff (w e. z -> w e. x)
10	9, 1	wal 1584	. . . 4 wff A.w(w e. z -> w e. x)
11		vy	. . . . . 6 set y
12	11	cv 1585	. . . . 5 class y
13	4, 12	wcel 1588	. . . 4 wff z e. y
14	10, 13	wi 3	. . 3 wff (A.w(w e. z -> w e. x) -> z e. y)
15	14, 3	wal 1584	. 2 wff A.z(A.w(w e. z -> w e. x) -> z e. y)
16	15, 11	wex 1615	1 wff E.yA.z(A.w(w e. z -> w e. x) -> z e. y)

This axiom is referenced by:  zfpow 3650  axpow2 3651  dtru 3662

Copyright terms: Public domain