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

Theorem rabeq2i 3228
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 2722 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3145 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 264 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wcel 2030  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-rab 2950
This theorem is referenced by:  fvmptss  6331  tfis  7096  nqereu  9789  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  qustgpopn  21970  nbusgrf1o0  26315  finsumvtxdg2ssteplem3  26499  clwlksfclwwlk2wrd  27045  clwlksfclwwlk1hash  27047  clwlksfclwwlk  27049  frgrwopreglem2  27293  frgrwopreglem5lem  27300  resf1o  29633  ballotlem2  30678  reprsuc  30821  oddprm2  30861  hgt750lemb  30862  bnj1476  31043  bnj1533  31048  bnj1538  31051  bnj1523  31265  cvmlift2lem12  31422  neibastop2lem  32480  topdifinfindis  33324  topdifinffinlem  33325  stoweidlem24  40559  stoweidlem31  40566  stoweidlem52  40587  stoweidlem54  40589  stoweidlem57  40592  salexct  40870  ovolval5lem3  41189  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  smfsuplem1  41338  smfsuplem3  41340  smfliminflem  41357
  Copyright terms: Public domain W3C validator