MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexrab Structured version   Visualization version   Unicode version

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
StepHypRef Expression
1 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
21elrab 3198 . . . 4  |-  ( x  e.  { y  e.  A  |  ph }  <->  ( x  e.  A  /\  ps ) )
32anbi1i 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 ) ) )
53, 4bitri 253 . 2  |-  ( ( x  e.  { y  e.  A  |  ph }  /\  ch )  <->  ( x  e.  A  /\  ( ps  /\  ch ) ) )
65rexbii2 2889 1  |-  ( E. x  e.  { y  e.  A  |  ph } ch  <->  E. x  e.  A  ( ps  /\  ch )
)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator