Theorem rabeq 3434

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  {crab 3419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420

This theorem is referenced by:  rabeqdv  3435  difeq1  4099  ineq1  4193  ifeq1  4509  ifeq2  4510  elfvmptrab  7025  supp0  8172  supeq2  9470  oieq2  9535  scott0  9908  mrcfval  17623  ipoval  18545  mndpsuppss  18748  psgnfval  19487  rgspnval  20581  dsmmelbas  21714  psrval  21890  ltbval  22016  opsrval  22019  m1detdiag  22552  isptfin  23471  islocfin  23472  kqval  23681  incistruhgr  29025  uvtx0  29340  vtxdg0e  29421  1hevtxdg1  29453  hashecclwwlkn1  30025  umgrhashecclwwlk  30026  ordtrestNEW  33895  ordtrest2NEWlem  33896  omsval  34270  orrvcval4  34442  orrvcoel  34443  orrvccel  34444  funray  36116  fvray  36117  itg2addnclem2  37654  cntotbnd  37778  lcfr  41562  hlhilocv  41938  pellfundval  42869  elmnc  43126  rfovd  43991  fsovd  43998  fsovcnvlem  44003  ntrneibex  44063  dvnprodlem2  45934  dvnprodlem3  45935  dvnprod  45936  fvmptrab  47277  rmsuppss  48259  scmsuppss  48260  dmatALTbas  48291