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  33894  ordtrest2NEWlem  33895  omsval  34267  orrvcval4  34439  orrvcoel  34440  orrvccel  34441  funray  36124  fvray  36125  itg2addnclem2  37662  cntotbnd  37786  lcfr  41574  hlhilocv  41946  pellfundval  42863  elmnc  43119  rfovd  43984  fsovd  43991  fsovcnvlem  43996  ntrneibex  44056  dvnprodlem2  45938  dvnprodlem3  45939  dvnprod  45940  fvmptrab  47286  rmsuppss  48364  scmsuppss  48365  dmatALTbas  48396