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

Theorem rabeqi 3392
Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3391. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2141, ax-11 2158, ax-12 2175. (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 627 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜑))
43rabbia2 3387 1 {𝑥𝐴𝜑} = {𝑥𝐵𝜑}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2110  {crab 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070
This theorem is referenced by:  rabrabiOLD  3404  f1ossf1o  6943  hsmex2  10047  iooval2  12968  fzval2  13098  phimullem  16332  pmtrsn  18911  dsmmbas2  20699  qtopres  22595  uvtxval  27475  cusgredg  27512  cffldtocusgr  27535  vtxdginducedm1  27631  finsumvtxdg2size  27638  konigsbergiedgw  28331  extwwlkfab  28435  zartopn  31539  satf0  33047  prjspeclsp  40159  k0004val0  41441  smflimlem4  43981  smfliminf  44036
  Copyright terms: Public domain W3C validator