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	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	|- y
1		vz	|- z
2		vw	|- w
3	2	cv	|- w
4	1	cv	|- z
5	3 4	wcel	|- w e. z
6		vx	|- x
7	6	cv	|- x
8	3 7	wcel	|- w e. x
9	5 8	wi	|- ( w e. z -> w e. x )
10	9 2	wal	|- A. w ( w e. z -> w e. x )
11	0	cv	|- y
12	4 11	wcel	|- z e. y
13	10 12	wi	|- ( A. w ( w e. z -> w e. x ) -> z e. y )
14	13 1	wal	|- A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
15	14 0	wex	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )