Theorem rabeqi 3406

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3405. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2139, ax-11 2156, ax-12 2173. (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 623	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3401	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1539   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  rabrabiOLD  3418  f1ossf1o  6982  hsmex2  10120  iooval2  13041  fzval2  13171  phimullem  16408  pmtrsn  19042  dsmmbas2  20854  qtopres  22757  uvtxval  27657  cusgredg  27694  cffldtocusgr  27717  vtxdginducedm1  27813  finsumvtxdg2size  27820  konigsbergiedgw  28513  extwwlkfab  28617  zartopn  31727  satf0  33234  prjspeclsp  40372  k0004val0  41653  smflimlem4  44196  smfliminf  44251