Theorem rabeq 3423

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (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 2818	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3410	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3408

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  rabeqdv  3424  difeq1  4085  ineq1  4179  ifeq1  4495  ifeq2  4496  elfvmptrab  7000  supp0  8147  supeq2  9406  oieq2  9473  scott0  9846  mrcfval  17576  ipoval  18496  mndpsuppss  18699  psgnfval  19437  rgspnval  20528  dsmmelbas  21655  psrval  21831  ltbval  21957  opsrval  21960  m1detdiag  22491  isptfin  23410  islocfin  23411  kqval  23620  incistruhgr  29013  uvtx0  29328  vtxdg0e  29409  1hevtxdg1  29441  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  ordtrestNEW  33918  ordtrest2NEWlem  33919  omsval  34291  orrvcval4  34463  orrvcoel  34464  orrvccel  34465  funray  36135  fvray  36136  itg2addnclem2  37673  cntotbnd  37797  lcfr  41586  hlhilocv  41958  pellfundval  42875  elmnc  43132  rfovd  43997  fsovd  44004  fsovcnvlem  44009  ntrneibex  44069  dvnprodlem2  45952  dvnprodlem3  45953  dvnprod  45954  fvmptrab  47297  rmsuppss  48362  scmsuppss  48363  dmatALTbas  48394