Theorem abrexexd

Description: Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	abrexexd.0	|- F/_ x A
	abrexexd.1	|- ( ph -> A e. _V )
Assertion	abrexexd	|- ( ph -> { y | E. x e. A y = B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		abrexexd.0	|- F/_ x A
2		abrexexd.1	|- ( ph -> A e. _V )
3		rnopab	|- ran { <. x , y >. | ( x e. A /\ y = B ) } = { y | E. x ( x e. A /\ y = B ) }
4		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
5	4	rneqi	|- ran ( x e. A |-> B ) = ran { <. x , y >. | ( x e. A /\ y = B ) }
6		df-rex	|- ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7	6	abbii	|- { y | E. x e. A y = B } = { y | E. x ( x e. A /\ y = B ) }
8	3 5 7	3eqtr4i	|- ran ( x e. A |-> B ) = { y | E. x e. A y = B }
9		funmpt	|- Fun ( x e. A |-> B )
10		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
11	10	dmmpt	|- dom ( x e. A |-> B ) = { x e. A | B e. _V }
12	1	rabexgfGS	|- ( A e. _V -> { x e. A | B e. _V } e. _V )
13	11 12	eqeltrid	|- ( A e. _V -> dom ( x e. A |-> B ) e. _V )
14		funex	|- ( ( Fun ( x e. A |-> B ) /\ dom ( x e. A |-> B ) e. _V ) -> ( x e. A |-> B ) e. _V )
15	9 13 14	sylancr	|- ( A e. _V -> ( x e. A |-> B ) e. _V )
16		rnexg	|- ( ( x e. A |-> B ) e. _V -> ran ( x e. A |-> B ) e. _V )
17	2 15 16	3syl	|- ( ph -> ran ( x e. A |-> B ) e. _V )
18	8 17	eqeltrrid	|- ( ph -> { y | E. x e. A y = B } e. _V )