Theorem rabeqi 3447

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434

This theorem is referenced by:  rabrabiOLD  3459  f1ossf1o  7148  hsmex2  10471  iooval2  13417  fzval2  13547  phimullem  16813  pmtrsn  19552  dsmmbas2  21775  qtopres  23722  left1s  27948  right1s  27949  uvtxval  29419  cusgredg  29456  cffldtocusgr  29479  cffldtocusgrOLD  29480  vtxdginducedm1  29576  finsumvtxdg2size  29583  konigsbergiedgw  30277  extwwlkfab  30381  zartopn  33836  satf0  35357  prjspeclsp  42599  k0004val0  44144  smflimlem4  46730  smfliminf  46787  isubgr0uhgr  47797  uspgrlimlem2  47892  uspgrlim  47895