Theorem rabeqi 3483

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf 3482. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2141 and ax-11 2156. (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 1798	. . . 4 ⊢ Ⅎ𝑥 𝐴 = 𝐵
3		eleq2 2901	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi1d 631	. . . 4 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
5	2, 4	abbid 2887	. . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)})
6		df-rab 3147	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
7		df-rab 3147	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	5, 6, 7	3eqtr4g 2881	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
9	1, 8	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}

Syntax hints:   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {cab 2799  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147

This theorem is referenced by:  rabrabi  3494  f1ossf1o  6885  hsmex2  9849  iooval2  12765  fzval2  12889  phimullem  16110  pmtrsn  18641  dsmmbas2  20875  qtopres  22300  uvtxval  27163  cusgredg  27200  cffldtocusgr  27223  vtxdginducedm1  27319  finsumvtxdg2size  27326  konigsbergiedgw  28021  extwwlkfab  28125  satf0  32614  prjspeclsp  39255  k0004val0  40497  smflimlem4  43043  smfliminf  43098