Theorem rabeq 3432

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419

This theorem is used by:  rabeqdv  3433  difeq1  4074  ineq1  4166  ifeq1  4493  ifeq2  4494  elfvmptrab  7023  supp0  8167  supeq2  9415  oieq2  9482  scott0OLD  9874  mrcfval  17688  ipoval  18610  chneq2  18693  mndpsuppss  18862  psgnfval  19616  rgspnval  20763  dsmmelbas  21941  psrval  22117  ltbval  22246  opsrval  22249  m1detdiag  22806  isptfin  23726  islocfin  23727  kqval  23936  incistruhgr  29486  uvtx0  29804  vtxdg0e  29884  1hevtxdg1  29916  hashecclwwlkn1  30497  umgrhashecclwwlk  30498  ordtrestNEW  34377  ordtrest2NEWlem  34378  omsval  34750  orrvcval4  34922  orrvcoel  34923  orrvccel  34924  funray  36671  fvray  36672  itg2addnclem2  38382  cntotbnd  38507  lcfr  42419  hlhilocv  42791  pellfundval  43667  elmnc  43923  rfovd  44787  fsovd  44794  fsovcnvlem  44799  ntrneibex  44859  dvnprodlem2  46721  dvnprodlem3  46722  dvnprod  46723  fvmptrab  48089  rmsuppss  49209  scmsuppss  49210  dmatALTbas  49240