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

Theorem rabeq2i 2959
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 2497 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 2887 . 2  |-  ( x  e.  { x  e.  B  |  ph }  <->  ( x  e.  B  /\  ph ) )
42, 3bitri 249 1  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1362    e. wcel 1755   {crab 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-rab 2714
This theorem is referenced by:  fvmptss  5770  tfis  6454  nqereu  9085  rpnnen1lem1  10966  rpnnen1lem2  10967  rpnnen1lem3  10968  rpnnen1lem5  10970  divstgpopn  19531  resf1o  25854  ddemeas  26505  ballotlem2  26718  cvmlift2lem12  27050  neibastop2lem  28422  stoweidlem24  29662  stoweidlem31  29669  stoweidlem52  29690  stoweidlem54  29692  stoweidlem57  29695  clwlkfclwwlk2wrd  30356  clwlkfclwwlk1hash  30358  clwlkfclwwlk  30360  frgrawopreglem2  30481  frgrawopreg  30485  bnj1476  31539  bnj1533  31544  bnj1538  31547  bnj1523  31761
  Copyright terms: Public domain W3C validator