Theorem rabeqi 3419

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  f1ossf1o  7100  hsmex2  10386  iooval2  13339  fzval2  13471  phimullem  16749  pmtrsn  19449  dsmmbas2  21646  qtopres  23585  left1s  27806  right1s  27807  uvtxval  29314  cusgredg  29351  cffldtocusgr  29374  cffldtocusgrOLD  29375  vtxdginducedm1  29471  finsumvtxdg2size  29478  konigsbergiedgw  30177  extwwlkfab  30281  zartopn  33865  satf0  35359  prjspeclsp  42600  k0004val0  44143  smflimlem4  46772  smfliminf  46829  isubgr0uhgr  47873  uspgrlimlem2  47988  uspgrlim  47991