Theorem rabeqi 3414

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3435. (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 2829	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 625	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3404	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  f1ossf1o  7083  hsmex2  10355  iooval2  13306  fzval2  13438  phimullem  16718  pmtrsn  19463  dsmmbas2  21707  qtopres  23657  left1s  27906  right1s  27907  uvtxval  29476  cusgredg  29513  cffldtocusgr  29536  cffldtocusgrOLD  29537  vtxdginducedm1  29633  finsumvtxdg2size  29640  konigsbergiedgw  30339  extwwlkfab  30443  zartopn  34057  satf0  35592  prjspeclsp  42974  k0004val0  44514  smflimlem4  47136  smfliminf  47193  isubgr0uhgr  48237  uspgrlimlem2  48353  uspgrlim  48356