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

Theorem rabeq2i 3398
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 2829 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3290 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 278 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1543  wcel 2110  {crab 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070
This theorem is referenced by:  fvmptss  6830  tfis  7633  nqereu  10543  rpnnen1lem2  12573  rpnnen1lem1  12574  rpnnen1lem3  12575  rpnnen1lem5  12577  qustgpopn  23017  nbusgrf1o0  27457  finsumvtxdg2ssteplem3  27635  frgrwopreglem2  28396  frgrwopreglem5lem  28403  resf1o  30785  nsgqusf1olem2  31313  nsgqusf1olem3  31314  ballotlem2  32167  reprsuc  32307  oddprm2  32347  hgt750lemb  32348  bnj1476  32540  bnj1533  32545  bnj1538  32548  bnj1523  32764  cvmlift2lem12  32989  neibastop2lem  34286  topdifinfindis  35254  topdifinffinlem  35255  stoweidlem24  43240  stoweidlem31  43247  stoweidlem52  43268  stoweidlem54  43270  stoweidlem57  43273  salexct  43548  ovolval5lem3  43867  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  smfsuplem1  44016  smfsuplem3  44018  smfliminflem  44035  prprsprreu  44644
  Copyright terms: Public domain W3C validator