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

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
StepHypRef Expression
1 ralab.1 . . . . 5  |-  ( y  =  x  ->  ( ph 
<->  ps ) )
21elrab 3117 . . . 4  |-  ( x  e.  { y  e.  A  |  ph }  <->  ( x  e.  A  /\  ps ) )
32anbi1i 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 ) ) )
53, 4bitri 249 . 2  |-  ( ( x  e.  { y  e.  A  |  ph }  /\  ch )  <->  ( x  e.  A  /\  ( ps  /\  ch ) ) )
65rexbii2 2744 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 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
  Copyright terms: Public domain W3C validator