Theorem rexrab 3123

Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.)

Hypothesis

Ref	Expression
ralab.1	|- ( y = x -> ( ph <-> ps ) )

Assertion

Ref	Expression
rexrab	|- ( E. x e. { y e. A | ph } ch <-> E. x e. A ( ps /\ ch ) )

Distinct variable groups:   x, y   y, A   ps, y

Allowed substitution hints:   ph( x, y)   ps( x)   ch( x, y)   A( x)

Proof of Theorem rexrab

Step	Hyp	Ref	Expression
1		ralab.1	. . . . 5 |- ( y = x -> ( ph <-> ps ) )
2	1	elrab 3117	. . . 4 |- ( x e. { y e. A | ph } <-> ( x e. A /\ ps ) )
3	2	anbi1i 695	. . 3 |- ( ( x e. { y e. A | ph } /\ ch ) <-> ( ( x e. A /\ ps ) /\ ch ) )
4		anass 649	. . 3 |- ( ( ( x e. A /\ ps ) /\ ch ) <-> ( x e. A /\ ( ps /\ ch ) ) )
5	3, 4	bitri 249	. 2 |- ( ( x e. { y e. A | ph } /\ ch ) <-> ( x e. A /\ ( ps /\ ch ) ) )
6	5	rexbii2 2744	1 |- ( E. x e. { y e. A | ph } ch <-> E. x e. A ( ps /\ ch ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1756   E.wrex 2716   {crab 2719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-rab 2724  df-v 2974

This theorem is referenced by:  wereu2  4717  wdom2d  7795  enfin2i  8490  infm3  10289  pmtrfrn  15964  pgpssslw  16113  ellspd  18230  ellspdOLD  18231  1stcfb  19049  xkobval  19159  xkococn  19233  imasdsf1olem  19948  nbgraf1olem1  23350  cvmliftlem15  27187  wsuclem  27762  rexrabdioph  29132  hbtlem6  29485  rusgranumwlks  30574