Theorem rabeq 3403

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  rabeqdv  3404  difeq1  4059  ineq1  4153  ifeq1  4470  ifeq2  4471  elfvmptrab  6977  supp0  8115  supeq2  9361  oieq2  9428  scott0  9810  mrcfval  17574  ipoval  18496  chneq2  18579  mndpsuppss  18733  psgnfval  19475  rgspnval  20589  dsmmelbas  21719  psrval  21895  ltbval  22021  opsrval  22024  m1detdiag  22562  isptfin  23481  islocfin  23482  kqval  23691  incistruhgr  29148  uvtx0  29463  vtxdg0e  29543  1hevtxdg1  29575  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  ordtrestNEW  34065  ordtrest2NEWlem  34066  omsval  34437  orrvcval4  34609  orrvcoel  34610  orrvccel  34611  funray  36322  fvray  36323  itg2addnclem2  37993  cntotbnd  38117  lcfr  42031  hlhilocv  42403  pellfundval  43308  elmnc  43564  rfovd  44428  fsovd  44435  fsovcnvlem  44440  ntrneibex  44500  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  fvmptrab  47740  rmsuppss  48846  scmsuppss  48847  dmatALTbas  48877