Theorem rabeqi 3429

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3451. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2141, ax-11 2157, ax-12 2177. (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 3418	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3415

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  f1ossf1o  7118  hsmex2  10447  iooval2  13395  fzval2  13527  phimullem  16798  pmtrsn  19500  dsmmbas2  21697  qtopres  23636  left1s  27858  right1s  27859  uvtxval  29366  cusgredg  29403  cffldtocusgr  29426  cffldtocusgrOLD  29427  vtxdginducedm1  29523  finsumvtxdg2size  29530  konigsbergiedgw  30229  extwwlkfab  30333  zartopn  33906  satf0  35394  prjspeclsp  42635  k0004val0  44178  smflimlem4  46803  smfliminf  46860  isubgr0uhgr  47886  uspgrlimlem2  48001  uspgrlim  48004