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

Theorem rabeq2i 3106
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
Assertion
Ref Expression
rabeq2i

Proof of Theorem rabeq2i
StepHypRef Expression
1 rabeqi.1 . . 3
21eleq2i 2535 . 2
3 rabid 3034 . 2
42, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  {crab 2811
This theorem is referenced by:  fvmptss  5964  tfis  6689  nqereu  9328  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  qustgpopn  20618  clwlkfclwwlk2wrd  24840  clwlkfclwwlk1hash  24842  clwlkfclwwlk  24844  frgrawopreglem2  25045  frgrawopreg  25049  resf1o  27553  ballotlem2  28427  cvmlift2lem12  28759  neibastop2lem  30178  stoweidlem24  31806  stoweidlem31  31813  stoweidlem52  31834  stoweidlem54  31836  stoweidlem57  31839  bnj1476  33905  bnj1533  33910  bnj1538  33913  bnj1523  34127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-rab 2816
  Copyright terms: Public domain W3C validator