Theorem rabeq 3409

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 3396	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

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

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 3395

This theorem is referenced by:  rabeqdv  3410  difeq1  4070  ineq1  4164  ifeq1  4480  ifeq2  4481  elfvmptrab  6959  supp0  8098  supeq2  9338  oieq2  9405  scott0  9782  mrcfval  17514  ipoval  18436  mndpsuppss  18639  psgnfval  19379  rgspnval  20497  dsmmelbas  21646  psrval  21822  ltbval  21948  opsrval  21951  m1detdiag  22482  isptfin  23401  islocfin  23402  kqval  23611  incistruhgr  29024  uvtx0  29339  vtxdg0e  29420  1hevtxdg1  29452  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  ordtrestNEW  33888  ordtrest2NEWlem  33889  omsval  34261  orrvcval4  34433  orrvcoel  34434  orrvccel  34435  funray  36118  fvray  36119  itg2addnclem2  37656  cntotbnd  37780  lcfr  41568  hlhilocv  41940  pellfundval  42857  elmnc  43113  rfovd  43978  fsovd  43985  fsovcnvlem  43990  ntrneibex  44050  dvnprodlem2  45932  dvnprodlem3  45933  dvnprod  45934  fvmptrab  47280  rmsuppss  48358  scmsuppss  48359  dmatALTbas  48390