Theorem rabeq 3430

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {crab 3415

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  rabeqdv  3431  difeq1  4094  ineq1  4188  ifeq1  4504  ifeq2  4505  elfvmptrab  7015  supp0  8164  supeq2  9460  oieq2  9527  scott0  9900  mrcfval  17620  ipoval  18540  mndpsuppss  18743  psgnfval  19481  rgspnval  20572  dsmmelbas  21699  psrval  21875  ltbval  22001  opsrval  22004  m1detdiag  22535  isptfin  23454  islocfin  23455  kqval  23664  incistruhgr  29058  uvtx0  29373  vtxdg0e  29454  1hevtxdg1  29486  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  ordtrestNEW  33952  ordtrest2NEWlem  33953  omsval  34325  orrvcval4  34497  orrvcoel  34498  orrvccel  34499  funray  36158  fvray  36159  itg2addnclem2  37696  cntotbnd  37820  lcfr  41604  hlhilocv  41976  pellfundval  42903  elmnc  43160  rfovd  44025  fsovd  44032  fsovcnvlem  44037  ntrneibex  44097  dvnprodlem2  45976  dvnprodlem3  45977  dvnprod  45978  fvmptrab  47321  rmsuppss  48345  scmsuppss  48346  dmatALTbas  48377