Theorem rabeqi 3403

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3424. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (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 2829	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 625	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3393	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391

This theorem is referenced by:  f1ossf1o  7077  hsmex2  10350  iooval2  13326  fzval2  13459  phimullem  16744  pmtrsn  19489  dsmmbas2  21731  qtopres  23677  left1s  27905  right1s  27906  uvtxval  29474  cusgredg  29511  cffldtocusgr  29534  cffldtocusgrOLD  29535  vtxdginducedm1  29631  finsumvtxdg2size  29638  konigsbergiedgw  30337  extwwlkfab  30441  zartopn  34039  satf0  35574  prjspeclsp  43063  k0004val0  44603  smflimlem4  47224  smfliminf  47281  isubgr0uhgr  48365  uspgrlimlem2  48481  uspgrlim  48484