Theorem rabeq 3415

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  rabeqdv  3416  difeq1  4073  ineq1  4167  ifeq1  4485  ifeq2  4486  elfvmptrab  6979  supp0  8117  supeq2  9363  oieq2  9430  scott0  9810  mrcfval  17543  ipoval  18465  chneq2  18548  mndpsuppss  18702  psgnfval  19441  rgspnval  20557  dsmmelbas  21706  psrval  21883  ltbval  22010  opsrval  22013  m1detdiag  22553  isptfin  23472  islocfin  23473  kqval  23682  incistruhgr  29164  uvtx0  29479  vtxdg0e  29560  1hevtxdg1  29592  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  ordtrestNEW  34099  ordtrest2NEWlem  34100  omsval  34471  orrvcval4  34643  orrvcoel  34644  orrvccel  34645  funray  36356  fvray  36357  itg2addnclem2  37923  cntotbnd  38047  lcfr  41961  hlhilocv  42333  pellfundval  43237  elmnc  43493  rfovd  44357  fsovd  44364  fsovcnvlem  44369  ntrneibex  44429  dvnprodlem2  46305  dvnprodlem3  46306  dvnprod  46307  fvmptrab  47652  rmsuppss  48730  scmsuppss  48731  dmatALTbas  48761