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 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 3397	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

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

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 3395

This theorem is referenced by:  f1ossf1o  7062  hsmex2  10327  iooval2  13281  fzval2  13413  phimullem  16690  pmtrsn  19398  dsmmbas2  21644  qtopres  23583  left1s  27809  right1s  27810  uvtxval  29332  cusgredg  29369  cffldtocusgr  29392  cffldtocusgrOLD  29393  vtxdginducedm1  29489  finsumvtxdg2size  29496  konigsbergiedgw  30192  extwwlkfab  30296  zartopn  33848  satf0  35355  prjspeclsp  42595  k0004val0  44137  smflimlem4  46765  smfliminf  46822  isubgr0uhgr  47867  uspgrlimlem2  47983  uspgrlim  47986