Theorem rabeq 3409

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  rabeqdv  3410  difeq1  4066  ineq1  4160  ifeq1  4476  ifeq2  4477  elfvmptrab  6958  supp0  8095  supeq2  9332  oieq2  9399  scott0  9779  mrcfval  17514  ipoval  18436  chneq2  18519  mndpsuppss  18673  psgnfval  19412  rgspnval  20527  dsmmelbas  21676  psrval  21852  ltbval  21978  opsrval  21981  m1detdiag  22512  isptfin  23431  islocfin  23432  kqval  23641  incistruhgr  29057  uvtx0  29372  vtxdg0e  29453  1hevtxdg1  29485  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  ordtrestNEW  33934  ordtrest2NEWlem  33935  omsval  34306  orrvcval4  34478  orrvcoel  34479  orrvccel  34480  funray  36184  fvray  36185  itg2addnclem2  37722  cntotbnd  37846  lcfr  41694  hlhilocv  42066  pellfundval  42983  elmnc  43239  rfovd  44104  fsovd  44111  fsovcnvlem  44116  ntrneibex  44176  dvnprodlem2  46055  dvnprodlem3  46056  dvnprod  46057  fvmptrab  47402  rmsuppss  48480  scmsuppss  48481  dmatALTbas  48512