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

Theorem rabeq2i 3183
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 𝐴 = {𝑥𝐵𝜑}
Assertion
Ref Expression
rabeq2i (𝑥𝐴 ↔ (𝑥𝐵𝜑))

Proof of Theorem rabeq2i
StepHypRef Expression
1 rabeq2i.1 . . 3 𝐴 = {𝑥𝐵𝜑}
21eleq2i 2690 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3106 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 264 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wcel 1987  {crab 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-rab 2916
This theorem is referenced by:  fvmptss  6249  tfis  7001  nqereu  9695  rpnnen1lem2  11758  rpnnen1lem1  11759  rpnnen1lem3  11760  rpnnen1lem5  11762  rpnnen1lem1OLD  11765  rpnnen1lem3OLD  11766  rpnnen1lem5OLD  11768  qustgpopn  21833  nbusgrf1o0  26158  clwlksfclwwlk2wrd  26824  clwlksfclwwlk1hash  26826  clwlksfclwwlk  26828  frgrwopreglem2  27040  frgrwopreg  27044  resf1o  29345  ballotlem2  30328  bnj1476  30622  bnj1533  30627  bnj1538  30630  bnj1523  30844  cvmlift2lem12  31001  neibastop2lem  31994  topdifinfindis  32823  topdifinffinlem  32824  stoweidlem24  39545  stoweidlem31  39552  stoweidlem52  39573  stoweidlem54  39575  stoweidlem57  39578  salexct  39856  ovolval5lem3  40172  pimdecfgtioc  40229  pimincfltioc  40230  pimdecfgtioo  40231  pimincfltioo  40232  smfsuplem1  40321  smfsuplem3  40323
  Copyright terms: Public domain W3C validator