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

Theorem rabeq2i 2968
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 2506 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 2896 . 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 1369    e. wcel 1756   {crab 2718
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-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-rab 2723
This theorem is referenced by:  fvmptss  5781  tfis  6464  nqereu  9097  rpnnen1lem1  10978  rpnnen1lem2  10979  rpnnen1lem3  10980  rpnnen1lem5  10982  divstgpopn  19689  resf1o  26029  ddemeas  26651  ballotlem2  26870  cvmlift2lem12  27202  neibastop2lem  28579  stoweidlem24  29817  stoweidlem31  29824  stoweidlem52  29845  stoweidlem54  29847  stoweidlem57  29850  clwlkfclwwlk2wrd  30511  clwlkfclwwlk1hash  30513  clwlkfclwwlk  30515  frgrawopreglem2  30636  frgrawopreg  30640  bnj1476  31838  bnj1533  31843  bnj1538  31846  bnj1523  32060
  Copyright terms: Public domain W3C validator