Theorem rabeq 3429

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  {crab 3415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416

This theorem is used by:  rabeqdv  3430  difeq1  4058  ineq1  4112  ifeq1  4488  ifeq2  4489  elfvmptrab  7031  supp0  8193  supeq2  9450  oieq2  9517  scott0OLD  9948  mrcfval  17794  ipoval  18716  chneq2  18799  mndpsuppss  18971  psgnfval  19726  rgspnval  20876  dsmmelbas  22057  psrval  22235  ltbval  22364  opsrval  22367  m1detdiag  22924  isptfin  23847  islocfin  23848  kqval  24057  incistruhgr  29669  uvtx0  29987  vtxdg0e  30067  1hevtxdg1  30099  hashecclwwlkn1  30680  umgrhashecclwwlk  30681  ordtrestNEW  34606  ordtrest2NEWlem  34607  omsval  34978  orrvcval4  35150  orrvcoel  35151  orrvccel  35152  funray  37032  fvray  37033  itg2addnclem2  38730  cntotbnd  38870  lcfr  42782  hlhilocv  43154  pellfundval  44027  elmnc  44278  rfovd  45141  fsovd  45148  fsovcnvlem  45153  ntrneibex  45213  dvnprodlem2  47096  dvnprodlem3  47097  dvnprod  47098  fvmptrab  48501  rmsuppss  49621  scmsuppss  49622  dmatALTbas  49652