Theorem rabeqi 3402

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3423. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (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 2828	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 625	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3392	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  f1ossf1o  7081  hsmex2  10355  iooval2  13331  fzval2  13464  phimullem  16749  pmtrsn  19494  dsmmbas2  21717  qtopres  23663  left1s  27887  right1s  27888  uvtxval  29456  cusgredg  29493  cffldtocusgr  29516  vtxdginducedm1  29612  finsumvtxdg2size  29619  konigsbergiedgw  30318  extwwlkfab  30422  zartopn  34019  satf0  35554  prjspeclsp  43045  k0004val0  44581  smflimlem4  47202  smfliminf  47259  isubgr0uhgr  48349  uspgrlimlem2  48465  uspgrlim  48468