Theorem rabeq 3417

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 2817	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3404	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  rabeqdv  3418  difeq1  4078  ineq1  4172  ifeq1  4488  ifeq2  4489  elfvmptrab  6979  supp0  8121  supeq2  9375  oieq2  9442  scott0  9815  mrcfval  17545  ipoval  18465  mndpsuppss  18668  psgnfval  19406  rgspnval  20497  dsmmelbas  21624  psrval  21800  ltbval  21926  opsrval  21929  m1detdiag  22460  isptfin  23379  islocfin  23380  kqval  23589  incistruhgr  28982  uvtx0  29297  vtxdg0e  29378  1hevtxdg1  29410  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  ordtrestNEW  33884  ordtrest2NEWlem  33885  omsval  34257  orrvcval4  34429  orrvcoel  34430  orrvccel  34431  funray  36101  fvray  36102  itg2addnclem2  37639  cntotbnd  37763  lcfr  41552  hlhilocv  41924  pellfundval  42841  elmnc  43098  rfovd  43963  fsovd  43970  fsovcnvlem  43975  ntrneibex  44035  dvnprodlem2  45918  dvnprodlem3  45919  dvnprod  45920  fvmptrab  47266  rmsuppss  48331  scmsuppss  48332  dmatALTbas  48363