vpwex

Description: Power set axiom: the powerclass of a set is a set. Axiom 4 of TakeutiZaring p. 17. (Contributed by NM, 30-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011) Revised to prove pwexg from vpwex . (Revised by BJ, 10-Aug-2022)

		Ref	Expression
	Assertion	vpwex	⊢ 𝒫 𝑥 ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-pw	⊢ 𝒫 𝑥 = { 𝑤 ∣ 𝑤 ⊆ 𝑥 }
2		axpow2	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦 )
3	2	sepexi	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 )
4		sseq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥 ) )
5	4	eqabbw	⊢ ( 𝑦 = { 𝑤 ∣ 𝑤 ⊆ 𝑥 } ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) )
6	5	exbii	⊢ ( ∃ 𝑦 𝑦 = { 𝑤 ∣ 𝑤 ⊆ 𝑥 } ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥 ) )
7	3 6	mpbir	⊢ ∃ 𝑦 𝑦 = { 𝑤 ∣ 𝑤 ⊆ 𝑥 }
8	7	issetri	⊢ { 𝑤 ∣ 𝑤 ⊆ 𝑥 } ∈ V
9	1 8	eqeltri	⊢ 𝒫 𝑥 ∈ V

Metamath Proof Explorer

Theorem vpwex

Proof