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

Theorem rabeqi 3419
Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3437. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2137, ax-11 2154, ax-12 2171. (Revised by Gino Giotto, 3-Jun-2024.)
Hypothesis
Ref Expression
rabeqi.1 𝐴 = 𝐵
Assertion
Ref Expression
rabeqi {𝑥𝐴𝜑} = {𝑥𝐵𝜑}

Proof of Theorem rabeqi
StepHypRef Expression
1 rabeqi.1 . . . 4 𝐴 = 𝐵
21eleq2i 2829 . . 3 (𝑥𝐴𝑥𝐵)
32anbi1i 624 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜑))
43rabbia2 3409 1 {𝑥𝐴𝜑} = {𝑥𝐵𝜑}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106  {crab 3406
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3407
This theorem is referenced by:  rabrabiOLD  3430  f1ossf1o  7071  hsmex2  10366  iooval2  13294  fzval2  13424  phimullem  16648  pmtrsn  19297  dsmmbas2  21139  qtopres  23045  left1s  27220  right1s  27221  uvtxval  28233  cusgredg  28270  cffldtocusgr  28293  vtxdginducedm1  28389  finsumvtxdg2size  28396  konigsbergiedgw  29090  extwwlkfab  29194  zartopn  32347  satf0  33857  prjspeclsp  40926  k0004val0  42406  smflimlem4  44985  smfliminf  45042
  Copyright terms: Public domain W3C validator