Metamath Proof Explorer


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 nfrex
 |-  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 )