Theorem 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	bm1.3ii	⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ⊆ 𝑥 )
4		abeq2	⊢ ( 𝑧 = { 𝑦 ∣ 𝑦 ⊆ 𝑥 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ⊆ 𝑥 ) )
5	4	exbii	⊢ ( ∃ 𝑧 𝑧 = { 𝑦 ∣ 𝑦 ⊆ 𝑥 } ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ⊆ 𝑥 ) )
6	3 5	mpbir	⊢ ∃ 𝑧 𝑧 = { 𝑦 ∣ 𝑦 ⊆ 𝑥 }
7	6	issetri	⊢ { 𝑦 ∣ 𝑦 ⊆ 𝑥 } ∈ V
8	1 7	eqeltri	⊢ 𝒫 𝑥 ∈ V