Theorem rabeqi 3410

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3431. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2146, ax-11 2162, ax-12 2182. (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 2825	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 624	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3400	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398

This theorem is referenced by:  f1ossf1o  7070  hsmex2  10334  iooval2  13288  fzval2  13420  phimullem  16700  pmtrsn  19441  dsmmbas2  21684  qtopres  23623  left1s  27850  right1s  27851  uvtxval  29376  cusgredg  29413  cffldtocusgr  29436  cffldtocusgrOLD  29437  vtxdginducedm1  29533  finsumvtxdg2size  29540  konigsbergiedgw  30239  extwwlkfab  30343  zartopn  33899  satf0  35427  prjspeclsp  42720  k0004val0  44261  smflimlem4  46886  smfliminf  46943  isubgr0uhgr  47987  uspgrlimlem2  48103  uspgrlim  48106