Axiom ax-pow 4843

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 4845 uses explicit subset notation. A version using class notation is pwex 4848. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
ax-pow	|- E. y A. 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	. . . . . . 7 setvar w
2		vz	. . . . . . 7 setvar z
3	1, 2	wel 1991	. . . . . 6 wff w e. z
4		vx	. . . . . . 7 setvar x
5	1, 4	wel 1991	. . . . . 6 wff w e. x
6	3, 5	wi 4	. . . . 5 wff ( w e. z -> w e. x )
7	6, 1	wal 1481	. . . 4 wff A. w ( w e. z -> w e. x )
8		vy	. . . . 5 setvar y
9	2, 8	wel 1991	. . . 4 wff z e. y
10	7, 9	wi 4	. . 3 wff ( A. w ( w e. z -> w e. x ) -> z e. y )
11	10, 2	wal 1481	. 2 wff A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
12	11, 8	wex 1704	1 wff E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

This axiom is referenced by:  zfpow  4844  axpow2  4845  bj-zfpow  32795