Axiom ax-pow 3918

Description: Axiom of Power Sets. An axiom of Intuitionistic 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. This is Axiom 8 of [Crosilla] p. "Axioms of CZF and IZF" except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 3869).

The variant axpow2 3920 uses explicit subset notation. A version using class notation is pwex 3923. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ax-pow	⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ 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 1391	. . . . . 6 wff w ∈ z
4		vx	. . . . . . 7 setvar x
5	1, 4	wel 1391	. . . . . 6 wff w ∈ x
6	3, 5	wi 4	. . . . 5 wff (w ∈ z → w ∈ x)
7	6, 1	wal 1240	. . . 4 wff ∀w(w ∈ z → w ∈ x)
8		vy	. . . . 5 setvar y
9	2, 8	wel 1391	. . . 4 wff z ∈ y
10	7, 9	wi 4	. . 3 wff (∀w(w ∈ z → w ∈ x) → z ∈ y)
11	10, 2	wal 1240	. 2 wff ∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
12	11, 8	wex 1378	1 wff ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)

This axiom is referenced by:  zfpow  3919  axpow2  3920