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

Theorem rabeq2i 3381
Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
Hypothesis
Ref Expression
rabeq2i.1 𝐴 = {𝑥𝐵𝜑}
Assertion
Ref Expression
rabeq2i (𝑥𝐴 ↔ (𝑥𝐵𝜑))

Proof of Theorem rabeq2i
StepHypRef Expression
1 rabeq2i.1 . . 3 𝐴 = {𝑥𝐵𝜑}
21eleq2i 2870 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3297 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 267 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385   = wceq 1653  wcel 2157  {crab 3093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-tru 1657  df-ex 1876  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-rab 3098
This theorem is referenced by:  fvmptss  6517  tfis  7288  nqereu  10039  rpnnen1lem2  12061  rpnnen1lem1  12062  rpnnen1lem3  12063  rpnnen1lem5  12065  qustgpopn  22251  nbusgrf1o0  26613  finsumvtxdg2ssteplem3  26797  clwlksfclwwlk2wrdOLD  27399  clwlksfclwwlk1hashOLD  27401  clwlksfclwwlkOLD  27403  frgrwopreglem2  27662  frgrwopreglem5lem  27669  resf1o  30023  ballotlem2  31067  reprsuc  31213  oddprm2  31253  hgt750lemb  31254  bnj1476  31434  bnj1533  31439  bnj1538  31442  bnj1523  31656  cvmlift2lem12  31813  neibastop2lem  32867  topdifinfindis  33692  topdifinffinlem  33693  stoweidlem24  40984  stoweidlem31  40991  stoweidlem52  41012  stoweidlem54  41014  stoweidlem57  41017  salexct  41295  ovolval5lem3  41614  pimdecfgtioc  41671  pimincfltioc  41672  pimdecfgtioo  41673  pimincfltioo  41674  smfsuplem1  41763  smfsuplem3  41765  smfliminflem  41782
  Copyright terms: Public domain W3C validator