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

Theorem rabeq2i 3170
 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 2680 . 2 (𝑥𝐴𝑥 ∈ {𝑥𝐵𝜑})
3 rabid 3095 . 2 (𝑥 ∈ {𝑥𝐵𝜑} ↔ (𝑥𝐵𝜑))
42, 3bitri 263 1 (𝑥𝐴 ↔ (𝑥𝐵𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rab 2905 This theorem is referenced by:  fvmptss  6201  tfis  6946  nqereu  9630  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  qustgpopn  21733  clwlkfclwwlk2wrd  26367  clwlkfclwwlk1hash  26369  clwlkfclwwlk  26371  frgrawopreglem2  26572  frgrawopreg  26576  resf1o  28893  ballotlem2  29877  bnj1476  30171  bnj1533  30176  bnj1538  30179  bnj1523  30393  cvmlift2lem12  30550  neibastop2lem  31525  topdifinfindis  32370  topdifinffinlem  32371  stoweidlem24  38917  stoweidlem31  38924  stoweidlem52  38945  stoweidlem54  38947  stoweidlem57  38950  salexct  39228  nbusgrf1o0  40597  clwlksfclwwlk2wrd  41265  clwlksfclwwlk1hash  41267  clwlksfclwwlk  41269  frgrwopreglem2  41482  frgrwopreg  41486
 Copyright terms: Public domain W3C validator