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

Theorem rabeq2i 3084
Description: Inference rule from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
Hypothesis
Ref Expression
rabeqi.1  |-  A  =  { x  e.  B  |  ph }
Assertion
Ref Expression
rabeq2i  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)

Proof of Theorem rabeq2i
StepHypRef Expression
1 rabeqi.1 . . 3  |-  A  =  { x  e.  B  |  ph }
21eleq2i 2507 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 3012 . 2  |-  ( x  e.  { x  e.  B  |  ph }  <->  ( x  e.  B  /\  ph ) )
42, 3bitri 252 1  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870   {crab 2786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-rab 2791
This theorem is referenced by:  fvmptss  5974  tfis  6695  nqereu  9353  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  qustgpopn  21065  clwlkfclwwlk2wrd  25413  clwlkfclwwlk1hash  25415  clwlkfclwwlk  25417  frgrawopreglem2  25618  frgrawopreg  25622  resf1o  28158  ballotlem2  29147  bnj1476  29446  bnj1533  29451  bnj1538  29454  bnj1523  29668  cvmlift2lem12  29825  neibastop2lem  30801  topdifinfindis  31483  topdifinffinlem  31484  stoweidlem24  37456  stoweidlem31  37464  stoweidlem52  37485  stoweidlem54  37487  stoweidlem57  37490
  Copyright terms: Public domain W3C validator