Theorem rabeq 3451

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 2830	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3438	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  rabeqdv  3452  difeq1  4119  ineq1  4213  ifeq1  4529  ifeq2  4530  elfvmptrab  7045  supp0  8190  supeq2  9488  oieq2  9553  scott0  9926  mrcfval  17651  ipoval  18575  mndpsuppss  18778  psgnfval  19518  rgspnval  20612  dsmmelbas  21759  psrval  21935  ltbval  22061  opsrval  22064  m1detdiag  22603  isptfin  23524  islocfin  23525  kqval  23734  incistruhgr  29096  uvtx0  29411  vtxdg0e  29492  1hevtxdg1  29524  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  ordtrestNEW  33920  ordtrest2NEWlem  33921  omsval  34295  orrvcval4  34467  orrvcoel  34468  orrvccel  34469  funray  36141  fvray  36142  itg2addnclem2  37679  cntotbnd  37803  lcfr  41587  hlhilocv  41963  pellfundval  42891  elmnc  43148  rfovd  44014  fsovd  44021  fsovcnvlem  44026  ntrneibex  44086  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  fvmptrab  47304  rmsuppss  48286  scmsuppss  48287  dmatALTbas  48318