Theorem rabeq 3411

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2146, ax-11 2162, ax-12 2182. (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 3399	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398

This theorem is referenced by:  rabeqdv  3412  difeq1  4069  ineq1  4163  ifeq1  4481  ifeq2  4482  elfvmptrab  6968  supp0  8105  supeq2  9349  oieq2  9416  scott0  9796  mrcfval  17529  ipoval  18451  chneq2  18534  mndpsuppss  18688  psgnfval  19427  rgspnval  20543  dsmmelbas  21692  psrval  21869  ltbval  21996  opsrval  21999  m1detdiag  22539  isptfin  23458  islocfin  23459  kqval  23668  incistruhgr  29101  uvtx0  29416  vtxdg0e  29497  1hevtxdg1  29529  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  ordtrestNEW  34027  ordtrest2NEWlem  34028  omsval  34399  orrvcval4  34571  orrvcoel  34572  orrvccel  34573  funray  36283  fvray  36284  itg2addnclem2  37812  cntotbnd  37936  lcfr  41784  hlhilocv  42156  pellfundval  43064  elmnc  43320  rfovd  44184  fsovd  44191  fsovcnvlem  44196  ntrneibex  44256  dvnprodlem2  46133  dvnprodlem3  46134  dvnprod  46135  fvmptrab  47480  rmsuppss  48558  scmsuppss  48559  dmatALTbas  48589