Theorem rabeq 3430

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  rabeqdv  3431  difeq1  4059  ineq1  4113  ifeq1  4489  ifeq2  4490  elfvmptrab  7054  supp0  8220  supeq2  9477  oieq2  9544  scott0OLD  9975  mrcfval  17832  ipoval  18754  chneq2  18837  mndpsuppss  19009  psgnfval  19765  rgspnval  20915  dsmmelbas  22100  psrval  22278  ltbval  22407  opsrval  22410  m1detdiag  22967  isptfin  23890  islocfin  23891  kqval  24100  incistruhgr  29714  uvtx0  30032  vtxdg0e  30112  1hevtxdg1  30144  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  ordtrestNEW  34664  ordtrest2NEWlem  34665  omsval  35036  orrvcval4  35208  orrvcoel  35209  orrvccel  35210  funray  37120  fvray  37121  itg2addnclem2  38858  cntotbnd  38996  lcfr  42908  hlhilocv  43280  pellfundval  44153  elmnc  44403  rfovd  45262  fsovd  45269  fsovcnvlem  45274  ntrneibex  45334  dvnprodlem2  47230  dvnprodlem3  47231  dvnprod  47232  fvmptrab  48635  rmsuppss  49813  scmsuppss  49814  dmatALTbas  49844