Theorem rabeq 3430

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2176, ax-11 2192, ax-12 2213. (Revised by GG, 20-Aug-2023.)

Assertion

Ref	Expression
rabeq	⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq

Step	Hyp	Ref	Expression
1		eleq2 2852	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 642	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3418	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417

This theorem is referenced by:  rabeqdv  3431  difeq1  4074  ineq1  4166  ifeq1  4491  ifeq2  4492  elfvmptrab  7019  supp0  8157  supeq2  9404  oieq2  9471  scott0  9856  mrcfval  17659  ipoval  18581  chneq2  18664  mndpsuppss  18818  psgnfval  19565  rgspnval  20711  dsmmelbas  21889  psrval  22065  ltbval  22194  opsrval  22197  m1detdiag  22754  isptfin  23673  islocfin  23674  kqval  23883  incistruhgr  29429  uvtx0  29744  vtxdg0e  29824  1hevtxdg1  29856  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  ordtrestNEW  34311  ordtrest2NEWlem  34312  omsval  34683  orrvcval4  34855  orrvcoel  34856  orrvccel  34857  funray  36632  fvray  36633  itg2addnclem2  38343  cntotbnd  38467  lcfr  42379  hlhilocv  42751  pellfundval  43627  elmnc  43883  rfovd  44747  fsovd  44754  fsovcnvlem  44759  ntrneibex  44819  dvnprodlem2  46681  dvnprodlem3  46682  dvnprod  46683  fvmptrab  48049  rmsuppss  49170  scmsuppss  49171  dmatALTbas  49201