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 2174, ax-11 2190, ax-12 2211. (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 2853	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 635	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3417	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1568   ∈ wcel 2141  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415

This theorem is referenced by:  f1ossf1o  7124  hsmex2  10416  iooval2  13404  fzval2  13537  phimullem  16837  pmtrsn  19588  dsmmbas2  21866  qtopres  23834  left1s  28064  right1s  28065  uvtxval  29703  cusgredg  29740  cffldtocusgr  29763  vtxdginducedm1  29859  finsumvtxdg2size  29866  konigsbergiedgw  30565  extwwlkfab  30669  zartopn  34231  satf0  35818  prjspeclsp  43292  k0004val0  44828  smflimlem4  47436  smfliminf  47493  isubgr0uhgr  48583  uspgrlimlem2  48699  uspgrlim  48702