Theorem rabeqi 3422

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3443. (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 2821	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 624	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3411	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  f1ossf1o  7103  hsmex2  10393  iooval2  13346  fzval2  13478  phimullem  16756  pmtrsn  19456  dsmmbas2  21653  qtopres  23592  left1s  27813  right1s  27814  uvtxval  29321  cusgredg  29358  cffldtocusgr  29381  cffldtocusgrOLD  29382  vtxdginducedm1  29478  finsumvtxdg2size  29485  konigsbergiedgw  30184  extwwlkfab  30288  zartopn  33872  satf0  35366  prjspeclsp  42607  k0004val0  44150  smflimlem4  46779  smfliminf  46836  isubgr0uhgr  47877  uspgrlimlem2  47992  uspgrlim  47995