Theorem rabeq 3408

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  rabeqdv  3409  difeq1  4046  ineq1  4136  ifeq1  4460  ifeq2  4461  elfvmptrab  6885  supp0  7953  supeq2  9137  oieq2  9202  scott0  9575  mrcfval  17234  ipoval  18163  psgnfval  19023  dsmmelbas  20856  psrval  21028  ltbval  21154  opsrval  21157  m1detdiag  21654  isptfin  22575  islocfin  22576  kqval  22785  incistruhgr  27352  uvtx0  27664  vtxdg0e  27744  1hevtxdg1  27776  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  ordtrestNEW  31773  ordtrest2NEWlem  31774  omsval  32160  orrvcval4  32331  orrvcoel  32332  orrvccel  32333  funray  34369  fvray  34370  itg2addnclem2  35756  cntotbnd  35881  lcfr  39526  hlhilocv  39902  pellfundval  40618  elmnc  40877  rgspnval  40909  rfovd  41498  fsovd  41505  fsovcnvlem  41510  ntrneibex  41572  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  dvnprod  43380  fvmptrab  44671  rmsuppss  45594  mndpsuppss  45595  scmsuppss  45596  dmatALTbas  45630