Theorem rexrab 3204

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 3198	. . . 4 |- ( x e. { y e. A | ph } <-> ( x e. A /\ ps ) )
3	2	anbi1i 702	. . 3 |- ( ( x e. { y e. A | ph } /\ ch ) <-> ( ( x e. A /\ ps ) /\ ch ) )
4		anass 655	. . 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 2889	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 1889   E.wrex 2740   {crab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rex 2745  df-rab 2748  df-v 3049

This theorem is referenced by:  wereu2  4834  wdom2d  8100  enfin2i  8756  infm3  10575  pmtrfrn  17111  pgpssslw  17278  ellspd  19372  1stcfb  20472  xkobval  20613  xkococn  20687  imasdsf1olem  21400  nbgraf1olem1  25181  rusgranumwlks  25696  cvmliftlem15  30033  wsuclem  30520  poimirlem4  31956  poimirlem26  31978  poimirlem27  31979  rexrabdioph  35649  hbtlem6  36000