Theorem rabeqi 3392

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3391. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2141, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 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 2829	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 627	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3387	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1543   ∈ wcel 2110  {crab 3065

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070

This theorem is referenced by:  rabrabiOLD  3404  f1ossf1o  6943  hsmex2  10047  iooval2  12968  fzval2  13098  phimullem  16332  pmtrsn  18911  dsmmbas2  20699  qtopres  22595  uvtxval  27475  cusgredg  27512  cffldtocusgr  27535  vtxdginducedm1  27631  finsumvtxdg2size  27638  konigsbergiedgw  28331  extwwlkfab  28435  zartopn  31539  satf0  33047  prjspeclsp  40159  k0004val0  41441  smflimlem4  43981  smfliminf  44036