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

Theorem rabeq2i 3325
 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 2819 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3242 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 264 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1620   ∈ wcel 2127  {crab 3042 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-12 2184  ax-ext 2728 This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1623  df-ex 1842  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-rab 3047 This theorem is referenced by:  fvmptss  6442  tfis  7207  nqereu  9914  rpnnen1lem2  11978  rpnnen1lem1  11979  rpnnen1lem3  11980  rpnnen1lem5  11982  rpnnen1lem1OLD  11985  rpnnen1lem3OLD  11986  rpnnen1lem5OLD  11988  qustgpopn  22095  nbusgrf1o0  26440  finsumvtxdg2ssteplem3  26624  clwlksfclwwlk2wrdOLD  27183  clwlksfclwwlk1hashOLD  27185  clwlksfclwwlkOLD  27187  frgrwopreglem2  27438  frgrwopreglem5lem  27445  resf1o  29785  ballotlem2  30830  reprsuc  30973  oddprm2  31013  hgt750lemb  31014  bnj1476  31195  bnj1533  31200  bnj1538  31203  bnj1523  31417  cvmlift2lem12  31574  neibastop2lem  32632  topdifinfindis  33476  topdifinffinlem  33477  stoweidlem24  40713  stoweidlem31  40720  stoweidlem52  40741  stoweidlem54  40743  stoweidlem57  40746  salexct  41024  ovolval5lem3  41343  pimdecfgtioc  41400  pimincfltioc  41401  pimdecfgtioo  41402  pimincfltioo  41403  smfsuplem1  41492  smfsuplem3  41494  smfliminflem  41511
 Copyright terms: Public domain W3C validator