Theorem rabeq 3427

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is used by:  rabeqdv  3428  difeq1  4067  ineq1  4159  ifeq1  4486  ifeq2  4487  elfvmptrab  7023  supp0  8182  supeq2  9440  oieq2  9507  scott0OLD  9938  mrcfval  17782  ipoval  18704  chneq2  18787  mndpsuppss  18959  psgnfval  19714  rgspnval  20864  dsmmelbas  22045  psrval  22223  ltbval  22352  opsrval  22355  m1detdiag  22912  isptfin  23835  islocfin  23836  kqval  24045  incistruhgr  29657  uvtx0  29975  vtxdg0e  30055  1hevtxdg1  30087  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  ordtrestNEW  34553  ordtrest2NEWlem  34554  omsval  34925  orrvcval4  35097  orrvcoel  35098  orrvccel  35099  funray  36905  fvray  36906  itg2addnclem2  38590  cntotbnd  38730  lcfr  42642  hlhilocv  43014  pellfundval  43886  elmnc  44137  rfovd  45000  fsovd  45007  fsovcnvlem  45012  ntrneibex  45072  dvnprodlem2  46956  dvnprodlem3  46957  dvnprod  46958  fvmptrab  48361  rmsuppss  49481  scmsuppss  49482  dmatALTbas  49512