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 2178, ax-11 2194, ax-12 2213. (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 1570   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  f1ossf1o  7117  hsmex2  10482  iooval2  13478  fzval2  13611  phimullem  16917  pmtrsn  19694  dsmmbas2  22004  qtopres  23978  left1s  28214  right1s  28215  uvtxval  29901  cusgredg  29938  cffldtocusgr  29961  vtxdginducedm1  30057  finsumvtxdg2size  30064  konigsbergiedgw  30782  extwwlkfab  30886  zartopn  34440  satf0  36058  prjspeclsp  43562  k0004val0  45098  smflimlem4  47706  smfliminf  47763  isubgr0uhgr  48893  uspgrlimlem2  49009  uspgrlim  49012