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

Theorem rabeq2i 3028
Description: Inference rule from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
Hypothesis
Ref Expression
rabeq2i.1  |-  A  =  { x  e.  B  |  ph }
Assertion
Ref Expression
rabeq2i  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)

Proof of Theorem rabeq2i
StepHypRef Expression
1 rabeq2i.1 . . 3  |-  A  =  { x  e.  B  |  ph }
21eleq2i 2541 . 2  |-  ( x  e.  A  <->  x  e.  { x  e.  B  |  ph } )
3 rabid 2953 . 2  |-  ( x  e.  { x  e.  B  |  ph }  <->  ( x  e.  B  /\  ph ) )
42, 3bitri 257 1  |-  ( x  e.  A  <->  ( x  e.  B  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   {crab 2760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-rab 2765
This theorem is referenced by:  fvmptss  5973  tfis  6700  nqereu  9372  rpnnen1lem1  11313  rpnnen1lem2  11314  rpnnen1lem3  11315  rpnnen1lem5  11317  qustgpopn  21212  clwlkfclwwlk2wrd  25647  clwlkfclwwlk1hash  25649  clwlkfclwwlk  25651  frgrawopreglem2  25852  frgrawopreg  25856  resf1o  28390  ballotlem2  29394  bnj1476  29730  bnj1533  29735  bnj1538  29738  bnj1523  29952  cvmlift2lem12  30109  neibastop2lem  31087  topdifinfindis  31819  topdifinffinlem  31820  stoweidlem24  37996  stoweidlem31  38004  stoweidlem52  38025  stoweidlem54  38027  stoweidlem57  38030  salexct  38305  nbusgrf1o0  39607
  Copyright terms: Public domain W3C validator