Theorem rabeq 3431

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 20-Aug-2023.)

Assertion

Ref	Expression
rabeq	⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq

Step	Hyp	Ref	Expression
1		eleq2 2878	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3423	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  rabeqdv  3432  difeq1  4043  ineq1  4131  ifeq1  4429  ifeq2  4430  elfvmptrab  6773  supp0  7818  supeq2  8896  oieq2  8961  scott0  9299  mrcfval  16871  ipoval  17756  psgnfval  18620  dsmmelbas  20428  psrval  20600  ltbval  20711  opsrval  20714  m1detdiag  21202  isptfin  22121  islocfin  22122  kqval  22331  incistruhgr  26872  uvtx0  27184  vtxdg0e  27264  1hevtxdg1  27296  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  ordtrestNEW  31274  ordtrest2NEWlem  31275  omsval  31661  orrvcval4  31832  orrvcoel  31833  orrvccel  31834  funray  33714  fvray  33715  itg2addnclem2  35109  cntotbnd  35234  lcfr  38881  hlhilocv  39253  pellfundval  39821  elmnc  40080  rgspnval  40112  rfovd  40702  fsovd  40709  fsovcnvlem  40714  ntrneibex  40776  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  dvnprod  42591  fvmptrab  43848  rmsuppss  44772  mndpsuppss  44773  scmsuppss  44774  dmatALTbas  44810