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 )

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 )

Metamath Proof Explorer