Theorem rabeqi 3406

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3427. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2154, ax-11 2170, ax-12 2191. (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 2833	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 631	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3396	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1548   ∈ wcel 2121  {crab 3393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394

This theorem is referenced by:  f1ossf1o  7074  hsmex2  10350  iooval2  13326  fzval2  13459  phimullem  16744  pmtrsn  19489  dsmmbas2  21716  qtopres  23685  left1s  27909  right1s  27910  uvtxval  29478  cusgredg  29515  cffldtocusgr  29538  vtxdginducedm1  29634  finsumvtxdg2size  29641  konigsbergiedgw  30340  extwwlkfab  30444  zartopn  34071  satf0  35615  prjspeclsp  43077  k0004val0  44613  smflimlem4  47231  smfliminf  47288  isubgr0uhgr  48378  uspgrlimlem2  48494  uspgrlim  48497