Theorem rabeq 3426

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  rabeqdv  3427  difeq1  4067  ineq1  4159  ifeq1  4486  ifeq2  4487  elfvmptrab  7017  supp0  8164  supeq2  9421  oieq2  9488  scott0OLD  9880  mrcfval  17699  ipoval  18621  chneq2  18704  mndpsuppss  18875  psgnfval  19630  rgspnval  20777  dsmmelbas  21955  psrval  22133  ltbval  22262  opsrval  22265  m1detdiag  22822  isptfin  23745  islocfin  23746  kqval  23955  incistruhgr  29539  uvtx0  29857  vtxdg0e  29937  1hevtxdg1  29969  hashecclwwlkn1  30550  umgrhashecclwwlk  30551  ordtrestNEW  34434  ordtrest2NEWlem  34435  omsval  34807  orrvcval4  34979  orrvcoel  34980  orrvccel  34981  funray  36723  fvray  36724  itg2addnclem2  38424  cntotbnd  38549  lcfr  42461  hlhilocv  42833  pellfundval  43724  elmnc  43980  rfovd  44844  fsovd  44851  fsovcnvlem  44856  ntrneibex  44916  dvnprodlem2  46778  dvnprodlem3  46779  dvnprod  46780  fvmptrab  48183  rmsuppss  49303  scmsuppss  49304  dmatALTbas  49334