HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Axiom ax-pow 2732
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 2734 states that the power set itself exists. A version using class notation is pwex 2735.
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
StepHypRef Expression
1 vw . . . . . . . 8 set w
21cv 952 . . . . . . 7 class w
3 vz . . . . . . . 8 set z
43cv 952 . . . . . . 7 class z
52, 4wcel 955 . . . . . 6 wff w e. z
6 vx . . . . . . . 8 set x
76cv 952 . . . . . . 7 class x
82, 7wcel 955 . . . . . 6 wff w e. x
95, 8wi 3 . . . . 5 wff (w e. z -> w e. x)
109, 1wal 951 . . . 4 wff A.w(w e. z -> w e. x)
11 vy . . . . . 6 set y
1211cv 952 . . . . 5 class y
134, 12wcel 955 . . . 4 wff z e. y
1410, 13wi 3 . . 3 wff (A.w(w e. z -> w e. x) -> z e. y)
1514, 3wal 951 . 2 wff A.z(A.w(w e. z -> w e. x) -> z e. y)
1615, 11wex 977 1 wff E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Colors of variables: wff set class
This axiom is referenced by:  axpow 2733  axpow2 2734  dtruALT 2738
Copyright terms: Public domain