Theorem rabeqi 3416

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3437. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (Revised by GG, 3-Jun-2024.)

Hypothesis

Ref	Expression
rabeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
rabeqi	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Proof of Theorem rabeqi

Step	Hyp	Ref	Expression
1		rabeqi.1	. . . 4 ⊢ 𝐴 = 𝐵
2	1	eleq2i 2820	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 624	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3405	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  f1ossf1o  7082  hsmex2  10362  iooval2  13315  fzval2  13447  phimullem  16725  pmtrsn  19433  dsmmbas2  21679  qtopres  23618  left1s  27844  right1s  27845  uvtxval  29367  cusgredg  29404  cffldtocusgr  29427  cffldtocusgrOLD  29428  vtxdginducedm1  29524  finsumvtxdg2size  29531  konigsbergiedgw  30227  extwwlkfab  30331  zartopn  33858  satf0  35352  prjspeclsp  42593  k0004val0  44136  smflimlem4  46765  smfliminf  46822  isubgr0uhgr  47866  uspgrlimlem2  47981  uspgrlim  47984