Theorem rexrab 3236

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 3230	. . . 4 |- ( x e. { y e. A | ph } <-> ( x e. A /\ ps ) )
3	2	anbi1i 700	. . 3 |- ( ( x e. { y e. A | ph } /\ ch ) <-> ( ( x e. A /\ ps ) /\ ch ) )
4		anass 654	. . 3 |- ( ( ( x e. A /\ ps ) /\ ch ) <-> ( x e. A /\ ( ps /\ ch ) ) )
5	3, 4	bitri 253	. 2 |- ( ( x e. { y e. A | ph } /\ ch ) <-> ( x e. A /\ ( ps /\ ch ) ) )
6	5	rexbii2 2926	1 |- ( E. x e. { y e. A | ph } ch <-> E. x e. A ( ps /\ ch ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   e. wcel 1869   E.wrex 2777   {crab 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-rab 2785  df-v 3084

This theorem is referenced by:  wereu2  4848  wdom2d  8099  enfin2i  8753  infm3  10570  pmtrfrn  17092  pgpssslw  17259  ellspd  19352  1stcfb  20452  xkobval  20593  xkococn  20667  imasdsf1olem  21380  nbgraf1olem1  25161  rusgranumwlks  25676  cvmliftlem15  30023  wsuclem  30509  poimirlem4  31902  poimirlem26  31924  poimirlem27  31925  rexrabdioph  35600  hbtlem6  35952