Theorem rabeqi 3425

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3445. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2177, ax-11 2193, ax-12 2212. (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 2852	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 636	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3415	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  f1ossf1o  7129  hsmex2  10511  iooval2  13509  fzval2  13642  phimullem  16956  pmtrsn  19733  dsmmbas2  22043  qtopres  24017  left1s  28281  right1s  28282  uvtxval  29968  cusgredg  30005  cffldtocusgr  30028  vtxdginducedm1  30124  finsumvtxdg2size  30131  konigsbergiedgw  30849  extwwlkfab  30953  zartopn  34549  satf0  36179  prjspeclsp  43683  k0004val0  45197  smflimlem4  47827  smfliminf  47884  isubgr0uhgr  49014  uspgrlimlem2  49130  uspgrlim  49133