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	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	⊢ 𝑦
1		vz	⊢ 𝑧
2		vw	⊢ 𝑤
3	2	cv	⊢ 𝑤
4	1	cv	⊢ 𝑧
5	3 4	wcel	⊢ 𝑤 ∈ 𝑧
6		vx	⊢ 𝑥
7	6	cv	⊢ 𝑥
8	3 7	wcel	⊢ 𝑤 ∈ 𝑥
9	5 8	wi	⊢ ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 )
10	9 2	wal	⊢ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 )
11	0	cv	⊢ 𝑦
12	4 11	wcel	⊢ 𝑧 ∈ 𝑦
13	10 12	wi	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
14	13 1	wal	⊢ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
15	14 0	wex	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )