Metamath Proof Explorer

Theorem abexssex

Description: Existence of a class abstraction with an existentially quantified expression. Both x and y can be free in ph . (Contributed by NM, 29-Jul-2006)

		Ref	Expression
	Hypotheses	abrexex2.1	$⊢ A \in V$
		abrexex2.2	$⊢ \{y \| φ\} \in V$
	Assertion	abexssex	$⊢ \{y \| \exists x (x \subseteq A \land φ)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		abrexex2.1	$⊢ A \in V$
2		abrexex2.2	$⊢ \{y \| φ\} \in V$
3		df-rex	$⊢ \exists x \in 𝒫 A φ \leftrightarrow \exists x (x \in 𝒫 A \land φ)$
4		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
5	4	anbi1i	$⊢ (x \in 𝒫 A \land φ) \leftrightarrow (x \subseteq A \land φ)$
6	5	exbii	$⊢ \exists x (x \in 𝒫 A \land φ) \leftrightarrow \exists x (x \subseteq A \land φ)$
7	3 6	bitri	$⊢ \exists x \in 𝒫 A φ \leftrightarrow \exists x (x \subseteq A \land φ)$
8	7	abbii	$⊢ \{y \| \exists x \in 𝒫 A φ\} = \{y \| \exists x (x \subseteq A \land φ)\}$
9	1	pwex	$⊢ 𝒫 A \in V$
10	9 2	abrexex2	$⊢ \{y \| \exists x \in 𝒫 A φ\} \in V$
11	8 10	eqeltrri	$⊢ \{y \| \exists x (x \subseteq A \land φ)\} \in V$