Theorem rabeq 3420

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

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

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 3406

This theorem is referenced by:  rabeqdv  3421  difeq1  4082  ineq1  4176  ifeq1  4492  ifeq2  4493  elfvmptrab  6997  supp0  8144  supeq2  9399  oieq2  9466  scott0  9839  mrcfval  17569  ipoval  18489  mndpsuppss  18692  psgnfval  19430  rgspnval  20521  dsmmelbas  21648  psrval  21824  ltbval  21950  opsrval  21953  m1detdiag  22484  isptfin  23403  islocfin  23404  kqval  23613  incistruhgr  29006  uvtx0  29321  vtxdg0e  29402  1hevtxdg1  29434  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  ordtrestNEW  33911  ordtrest2NEWlem  33912  omsval  34284  orrvcval4  34456  orrvcoel  34457  orrvccel  34458  funray  36128  fvray  36129  itg2addnclem2  37666  cntotbnd  37790  lcfr  41579  hlhilocv  41951  pellfundval  42868  elmnc  43125  rfovd  43990  fsovd  43997  fsovcnvlem  44002  ntrneibex  44062  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  fvmptrab  47293  rmsuppss  48358  scmsuppss  48359  dmatALTbas  48390