Theorem rabeqi 3479

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3478. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2144 and ax-11 2160. (Revised by Gino Giotto, 20-Aug-2023.)

Hypothesis

Ref	Expression
rabeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
rabeqi	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Proof of Theorem rabeqi

Step	Hyp	Ref	Expression
1		rabeqi.1	. 2 ⊢ 𝐴 = 𝐵
2	1	nfth 1801	. . . 4 ⊢ Ⅎ𝑥 𝐴 = 𝐵
3		eleq2 2900	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi1d 631	. . . 4 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
5	2, 4	abbid 2886	. . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)})
6		df-rab 3146	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
7		df-rab 3146	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	5, 6, 7	3eqtr4g 2880	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
9	1, 8	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   ∧ wa 398   = wceq 1536   ∈ wcel 2113  {cab 2798  {crab 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-rab 3146

This theorem is referenced by:  rabrabi  3490  f1ossf1o  6883  hsmex2  9848  iooval2  12765  fzval2  12892  phimullem  16111  pmtrsn  18642  dsmmbas2  20876  qtopres  22301  uvtxval  27167  cusgredg  27204  cffldtocusgr  27227  vtxdginducedm1  27323  finsumvtxdg2size  27330  konigsbergiedgw  28025  extwwlkfab  28129  satf0  32640  prjspeclsp  39338  k0004val0  40578  smflimlem4  43124  smfliminf  43179