Theorem rabeqi 3410

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3397

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398

This theorem is referenced by:  f1ossf1o  7071  hsmex2  10341  iooval2  13292  fzval2  13424  phimullem  16704  pmtrsn  19446  dsmmbas2  21690  qtopres  23640  left1s  27867  right1s  27868  uvtxval  29409  cusgredg  29446  cffldtocusgr  29469  cffldtocusgrOLD  29470  vtxdginducedm1  29566  finsumvtxdg2size  29573  konigsbergiedgw  30272  extwwlkfab  30376  zartopn  33981  satf0  35515  prjspeclsp  42797  k0004val0  44337  smflimlem4  46960  smfliminf  47017  isubgr0uhgr  48061  uspgrlimlem2  48177  uspgrlim  48180