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 e. _V
	abrexex2.2	|- { y | ph } e. _V
Assertion	abrexex2	|- { y | E. x e. A ph } e. _V

Proof

Step	Hyp	Ref	Expression
1		abrexex2.1	|- A e. _V
2		abrexex2.2	|- { y | ph } e. _V
3	2	rgenw	|- A. x e. A { y | ph } e. _V
4		abrexex2g	|- ( ( A e. _V /\ A. x e. A { y | ph } e. _V ) -> { y | E. x e. A ph } e. _V )
5	1 3 4	mp2an	|- { y | E. x e. A ph } e. _V