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

Theorem rabeqi 3429
 Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3428. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2142, 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 2881 . . 3 (𝑥𝐴𝑥𝐵)
32anbi1i 626 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜑))
43rabbia2 3424 1 {𝑥𝐴𝜑} = {𝑥𝐵𝜑}
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∈ wcel 2111  {crab 3110 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115 This theorem is referenced by:  rabrabi  3440  f1ossf1o  6868  hsmex2  9847  iooval2  12762  fzval2  12891  phimullem  16109  pmtrsn  18643  dsmmbas2  20431  qtopres  22313  uvtxval  27187  cusgredg  27224  cffldtocusgr  27247  vtxdginducedm1  27343  finsumvtxdg2size  27350  konigsbergiedgw  28043  extwwlkfab  28147  zartopn  31243  satf0  32747  prjspeclsp  39649  k0004val0  40900  smflimlem4  43450  smfliminf  43505
 Copyright terms: Public domain W3C validator