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

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

Proof of Theorem reqabi
StepHypRef Expression
1 reqabi.1 . . 3 𝐴 = {𝑥𝐵𝜑}
21eleq2i 2833 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3458 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 275 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  {crab 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437
This theorem is referenced by:  fvmptss  7028  tfis  7876  nqereu  10969  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  qustgpopn  24128  addsproplem2  28003  sleadd1  28022  negsproplem6  28065  negsid  28073  nbusgrf1o0  29386  finsumvtxdg2ssteplem3  29565  frgrwopreglem2  30332  frgrwopreglem5lem  30339  resf1o  32741  elrgspnlem4  33249  nsgqusf1olem2  33442  nsgqusf1olem3  33443  ballotlem2  34491  reprsuc  34630  oddprm2  34670  hgt750lemb  34671  bnj1476  34861  bnj1533  34866  bnj1538  34869  bnj1523  35085  cvmlift2lem12  35319  neibastop2lem  36361  topdifinfindis  37347  topdifinffinlem  37348  stoweidlem24  46039  stoweidlem31  46046  stoweidlem52  46067  stoweidlem54  46069  stoweidlem57  46072  salexct  46349  ovolval5lem3  46669  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  smfsuplem1  46826  smfsuplem3  46828  smfliminflem  46845  prprsprreu  47506
  Copyright terms: Public domain W3C validator