Axiom ax-pow 4311

Description: Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the power set of a given set 𝑥 i.e. contains every subset of 𝑥. 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 4254).

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

Assertion

Ref	Expression
ax-pow	⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Detailed syntax breakdown of Axiom ax-pow

Step	Hyp	Ref	Expression
1		vw	. . . . . . 7 setvar 𝑤
2		vz	. . . . . . 7 setvar 𝑧
3	1, 2	wel 2210	. . . . . 6 wff 𝑤 ∈ 𝑧
4		vx	. . . . . . 7 setvar 𝑥
5	1, 4	wel 2210	. . . . . 6 wff 𝑤 ∈ 𝑥
6	3, 5	wi 4	. . . . 5 wff (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
7	6, 1	wal 1400	. . . 4 wff ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
8		vy	. . . . 5 setvar 𝑦
9	2, 8	wel 2210	. . . 4 wff 𝑧 ∈ 𝑦
10	7, 9	wi 4	. . 3 wff (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
11	10, 2	wal 1400	. 2 wff ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
12	11, 8	wex 1545	1 wff ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

This axiom is used by:  zfpow  4312  axpow2  4313