Metamath Proof Explorer

Theorem abrexex2

Description: Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x and y . See also abrexex . (Contributed by NM, 12-Sep-2004)

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

Proof

Step	Hyp	Ref	Expression
1		abrexex2.1	$⊢ A \in V$
2		abrexex2.2	$⊢ \{y \| φ\} \in V$
3	2	rgenw	$⊢ \forall x \in A \{y \| φ\} \in V$
4		abrexex2g	$⊢ (A \in V \land \forall x \in A \{y \| φ\} \in V) \to \{y \| \exists x \in A φ\} \in V$
5	1 3 4	mp2an	$⊢ \{y \| \exists x \in A φ\} \in V$