Theorem rabeqi 3412

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400

This theorem is referenced by:  f1ossf1o  7073  hsmex2  10345  iooval2  13296  fzval2  13428  phimullem  16708  pmtrsn  19450  dsmmbas2  21694  qtopres  23644  left1s  27893  right1s  27894  uvtxval  29462  cusgredg  29499  cffldtocusgr  29522  cffldtocusgrOLD  29523  vtxdginducedm1  29619  finsumvtxdg2size  29626  konigsbergiedgw  30325  extwwlkfab  30429  zartopn  34034  satf0  35568  prjspeclsp  42876  k0004val0  44416  smflimlem4  47039  smfliminf  47096  isubgr0uhgr  48140  uspgrlimlem2  48256  uspgrlim  48259