Theorem rabeqi 3416

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3415. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2137, ax-11 2154, ax-12 2171. (Revised by Gino Giotto, 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 2830	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 624	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3412	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1539   ∈ wcel 2106  {crab 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073

This theorem is referenced by:  rabrabiOLD  3428  f1ossf1o  7000  hsmex2  10189  iooval2  13112  fzval2  13242  phimullem  16480  pmtrsn  19127  dsmmbas2  20944  qtopres  22849  uvtxval  27754  cusgredg  27791  cffldtocusgr  27814  vtxdginducedm1  27910  finsumvtxdg2size  27917  konigsbergiedgw  28612  extwwlkfab  28716  zartopn  31825  satf0  33334  prjspeclsp  40451  k0004val0  41764  smflimlem4  44309  smfliminf  44364