Theorem abrexex2g

Description: Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	abrexex2g	|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { y | E. x e. A ph } e. _V )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ z E. x e. A ph
2		nfcv	|- F/_ y A
3		nfs1v	|- F/ y [ z / y ] ph
4	2 3	nfrexw	|- F/ y E. x e. A [ z / y ] ph
5		sbequ12	|- ( y = z -> ( ph <-> [ z / y ] ph ) )
6	5	rexbidv	|- ( y = z -> ( E. x e. A ph <-> E. x e. A [ z / y ] ph ) )
7	1 4 6	cbvabw	|- { y | E. x e. A ph } = { z | E. x e. A [ z / y ] ph }
8		df-clab	|- ( z e. { y | ph } <-> [ z / y ] ph )
9	8	rexbii	|- ( E. x e. A z e. { y | ph } <-> E. x e. A [ z / y ] ph )
10	9	abbii	|- { z | E. x e. A z e. { y | ph } } = { z | E. x e. A [ z / y ] ph }
11	7 10	eqtr4i	|- { y | E. x e. A ph } = { z | E. x e. A z e. { y | ph } }
12		df-iun	|- U_ x e. A { y | ph } = { z | E. x e. A z e. { y | ph } }
13		iunexg	|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> U_ x e. A { y | ph } e. _V )
14	12 13	eqeltrrid	|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { z | E. x e. A z e. { y | ph } } e. _V )
15	11 14	eqeltrid	|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { y | E. x e. A ph } e. _V )