This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwexg

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003)

		Ref	Expression
	Assertion	pwexg	$⊢ A \in V \to 𝒫 A \in V$

Step	Hyp	Ref	Expression
1		pweq	$⊢ x = A \to 𝒫 x = 𝒫 A$
2	1	eleq1d	$⊢ x = A \to (𝒫 x \in V \leftrightarrow 𝒫 A \in V)$
3		vpwex	$⊢ 𝒫 x \in V$
4	2 3	vtoclg	$⊢ A \in V \to 𝒫 A \in V$