Theorem rabeqi 3429

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3450. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2177, ax-11 2193, ax-12 2214. (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 2856	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	2	anbi1i 633	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	3	rabbia2 3419	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   = wceq 1562   ∈ wcel 2144  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417

This theorem is referenced by:  f1ossf1o  7112  hsmex2  10392  iooval2  13384  fzval2  13517  phimullem  16816  pmtrsn  19561  dsmmbas2  21791  qtopres  23760  left1s  27990  right1s  27991  uvtxval  29590  cusgredg  29627  cffldtocusgr  29650  vtxdginducedm1  29746  finsumvtxdg2size  29753  konigsbergiedgw  30452  extwwlkfab  30556  zartopn  34174  satf0  35727  prjspeclsp  43199  k0004val0  44735  smflimlem4  47353  smfliminf  47410  isubgr0uhgr  48500  uspgrlimlem2  48616  uspgrlim  48619