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

Theorem rabeq2i 2896
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 2451 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 2827 . 2  |-  ( x  e.  { x  e.  B  |  ph }  <->  ( x  e.  B  /\  ph ) )
42, 3bitri 241 1  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   {crab 2653
This theorem is referenced by:  tfis  4774  fvmptss  5752  nqereu  8739  rpnnen1lem1  10532  rpnnen1lem2  10533  rpnnen1lem3  10534  rpnnen1lem5  10536  divstgpopn  18070  ballotlem2  24525  cvmlift2lem12  24780  neibastop2lem  26080  stoweidlem24  27441  stoweidlem31  27448  stoweidlem52  27469  stoweidlem54  27471  stoweidlem57  27474  frgrawopreglem2  27797  frgrawopreg  27801  bnj1476  28556  bnj1533  28561  bnj1538  28564  bnj1523  28778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-rab 2658
  Copyright terms: Public domain W3C validator