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  17549  ipoval  18471  mndpsuppss  18674  psgnfval  19414  rgspnval  20532  dsmmelbas  21681  psrval  21857  ltbval  21983  opsrval  21986  m1detdiag  22517  isptfin  23436  islocfin  23437  kqval  23646  incistruhgr  29059  uvtx0  29374  vtxdg0e  29455  1hevtxdg1  29487  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  ordtrestNEW  33904  ordtrest2NEWlem  33905  omsval  34277  orrvcval4  34449  orrvcoel  34450  orrvccel  34451  funray  36121  fvray  36122  itg2addnclem2  37659  cntotbnd  37783  lcfr  41572  hlhilocv  41944  pellfundval  42861  elmnc  43118  rfovd  43983  fsovd  43990  fsovcnvlem  43995  ntrneibex  44055  dvnprodlem2  45938  dvnprodlem3  45939  dvnprod  45940  fvmptrab  47286  rmsuppss  48351  scmsuppss  48352  dmatALTbas  48383