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	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. 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 e. z
4		vx	. . . . . . 7 set x
5	1, 4	wel 803	. . . . . 6 wff w e. x
6	3, 5	wi 2	. . . . 5 wff (w e. z -> w e. x)
7	6, 1	wal 672	. . . 4 wff A.w(w e. z -> w e. x)
8		vy	. . . . 5 set y
9	2, 8	wel 803	. . . 4 wff z e. y
10	7, 9	wi 2	. . 3 wff (A.w(w e. z -> w e. x) -> z e. y)
11	10, 2	wal 672	. 2 wff A.z(A.w(w e. z -> w e. x) -> z e. y)
12	11, 8	wex 678	1 wff E.yA.z(A.w(w e. z -> w e. x) -> z e. y)

This axiom is referenced by:  axpow 1082

metamath.org