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

Theorem rabeq2i 2798
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 2360 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 2729 . 2  |-  ( x  e.  { x  e.  B  |  ph }  <->  ( x  e.  B  /\  ph ) )
42, 3bitri 240 1  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   {crab 2560
This theorem is referenced by:  tfis  4661  fvmptss  5625  nqereu  8569  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  divstgpopn  17818  cvmlift2lem12  23860  neibastop2lem  26412  stoweidlem52  27904  bnj1476  29195  bnj1533  29200  bnj1538  29203  bnj1523  29417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-rab 2565
  Copyright terms: Public domain W3C validator