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

Theorem rabeq2i 3435
 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 2881 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3331 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 278 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115 This theorem is referenced by:  fvmptss  6758  tfis  7552  nqereu  10343  rpnnen1lem2  12367  rpnnen1lem1  12368  rpnnen1lem3  12369  rpnnen1lem5  12371  qustgpopn  22735  nbusgrf1o0  27169  finsumvtxdg2ssteplem3  27347  frgrwopreglem2  28108  frgrwopreglem5lem  28115  resf1o  30502  ballotlem2  31871  reprsuc  32011  oddprm2  32051  hgt750lemb  32052  bnj1476  32244  bnj1533  32249  bnj1538  32252  bnj1523  32468  cvmlift2lem12  32689  neibastop2lem  33836  topdifinfindis  34782  topdifinffinlem  34783  stoweidlem24  42709  stoweidlem31  42716  stoweidlem52  42737  stoweidlem54  42739  stoweidlem57  42742  salexct  43017  ovolval5lem3  43336  pimdecfgtioc  43393  pimincfltioc  43394  pimdecfgtioo  43395  pimincfltioo  43396  smfsuplem1  43485  smfsuplem3  43487  smfliminflem  43504  prprsprreu  44079
 Copyright terms: Public domain W3C validator