Theorem rabeq 3404

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 3392	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

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

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 3391

This theorem is referenced by:  rabeqdv  3405  difeq1  4060  ineq1  4154  ifeq1  4471  ifeq2  4472  elfvmptrab  6972  supp0  8109  supeq2  9355  oieq2  9422  scott0  9804  mrcfval  17568  ipoval  18490  chneq2  18573  mndpsuppss  18727  psgnfval  19469  rgspnval  20583  dsmmelbas  21732  psrval  21908  ltbval  22034  opsrval  22037  m1detdiag  22575  isptfin  23494  islocfin  23495  kqval  23704  incistruhgr  29165  uvtx0  29480  vtxdg0e  29561  1hevtxdg1  29593  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  ordtrestNEW  34084  ordtrest2NEWlem  34085  omsval  34456  orrvcval4  34628  orrvcoel  34629  orrvccel  34630  funray  36341  fvray  36342  itg2addnclem2  38010  cntotbnd  38134  lcfr  42048  hlhilocv  42420  pellfundval  43329  elmnc  43585  rfovd  44449  fsovd  44456  fsovcnvlem  44461  ntrneibex  44521  dvnprodlem2  46396  dvnprodlem3  46397  dvnprod  46398  fvmptrab  47755  rmsuppss  48861  scmsuppss  48862  dmatALTbas  48892