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

Theorem rabeq2i 2785
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 2347 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 2716 . 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 1623    e. wcel 1684   {crab 2547
This theorem is referenced by:  tfis  4645  fvmptss  5609  nqereu  8553  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  divstgpopn  17802  cvmlift2lem12  23845  neibastop2lem  26309  stoweidlem52  27801  bnj1476  28879  bnj1533  28884  bnj1538  28887  bnj1523  29101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-rab 2552
  Copyright terms: Public domain W3C validator