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

Theorem rabeq2i 3110
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 2545 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 3038 . 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 1379    e. wcel 1767   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-rab 2823
This theorem is referenced by:  fvmptss  5958  tfis  6673  nqereu  9307  rpnnen1lem1  11208  rpnnen1lem2  11209  rpnnen1lem3  11210  rpnnen1lem5  11212  divstgpopn  20381  clwlkfclwwlk2wrd  24544  clwlkfclwwlk1hash  24546  clwlkfclwwlk  24548  frgrawopreglem2  24750  frgrawopreg  24754  resf1o  27253  ddemeas  27876  ballotlem2  28095  cvmlift2lem12  28427  neibastop2lem  29809  stoweidlem24  31352  stoweidlem31  31359  stoweidlem52  31380  stoweidlem54  31382  stoweidlem57  31385  bnj1476  33002  bnj1533  33007  bnj1538  33010  bnj1523  33224
  Copyright terms: Public domain W3C validator