Theorem rabeqi 3457

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  rabrabiOLD  3469  f1ossf1o  7162  hsmex2  10502  iooval2  13440  fzval2  13570  phimullem  16826  pmtrsn  19561  dsmmbas2  21780  qtopres  23727  left1s  27951  right1s  27952  uvtxval  29422  cusgredg  29459  cffldtocusgr  29482  cffldtocusgrOLD  29483  vtxdginducedm1  29579  finsumvtxdg2size  29586  konigsbergiedgw  30280  extwwlkfab  30384  zartopn  33821  satf0  35340  prjspeclsp  42567  k0004val0  44116  smflimlem4  46695  smfliminf  46752  isubgr0uhgr  47743  uspgrlimlem2  47813  uspgrlim  47816