Theorem rabeqi 3427

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {crab 3414

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is used by:  f1ossf1o  7125  hsmex2  10438  iooval2  13433  fzval2  13566  phimullem  16874  pmtrsn  19647  dsmmbas2  21951  qtopres  23925  left1s  28158  right1s  28159  uvtxval  29833  cusgredg  29870  cffldtocusgr  29893  vtxdginducedm1  29989  finsumvtxdg2size  29996  konigsbergiedgw  30714  extwwlkfab  30818  zartopn  34372  satf0  35938  prjspeclsp  43445  k0004val0  44981  smflimlem4  47589  smfliminf  47646  isubgr0uhgr  48776  uspgrlimlem2  48892  uspgrlim  48895