Theorem rabeqi 3446

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434

This theorem is referenced by:  rabrabiOLD  3457  f1ossf1o  7126  hsmex2  10428  iooval2  13357  fzval2  13487  phimullem  16712  pmtrsn  19387  dsmmbas2  21292  qtopres  23202  left1s  27390  right1s  27391  uvtxval  28675  cusgredg  28712  cffldtocusgr  28735  vtxdginducedm1  28831  finsumvtxdg2size  28838  konigsbergiedgw  29532  extwwlkfab  29636  zartopn  32886  satf0  34394  gg-cffldtocusgr  35230  prjspeclsp  41402  k0004val0  42953  smflimlem4  45538  smfliminf  45595