Theorem rabeqi 3408

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3429. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2144, ax-11 2160, ax-12 2180. (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 2823	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 624	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3398	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  f1ossf1o  7061  hsmex2  10324  iooval2  13278  fzval2  13410  phimullem  16690  pmtrsn  19431  dsmmbas2  21674  qtopres  23613  left1s  27840  right1s  27841  uvtxval  29365  cusgredg  29402  cffldtocusgr  29425  cffldtocusgrOLD  29426  vtxdginducedm1  29522  finsumvtxdg2size  29529  konigsbergiedgw  30228  extwwlkfab  30332  zartopn  33888  satf0  35416  prjspeclsp  42715  k0004val0  44257  smflimlem4  46882  smfliminf  46939  isubgr0uhgr  47983  uspgrlimlem2  48099  uspgrlim  48102