Theorem rabeq 3448

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434

This theorem is referenced by:  rabeqdv  3449  difeq1  4129  ineq1  4221  ifeq1  4535  ifeq2  4536  elfvmptrab  7045  supp0  8189  supeq2  9486  oieq2  9551  scott0  9924  mrcfval  17653  ipoval  18588  mndpsuppss  18791  psgnfval  19533  rgspnval  20629  dsmmelbas  21777  psrval  21953  ltbval  22079  opsrval  22082  m1detdiag  22619  isptfin  23540  islocfin  23541  kqval  23750  incistruhgr  29111  uvtx0  29426  vtxdg0e  29507  1hevtxdg1  29539  hashecclwwlkn1  30106  umgrhashecclwwlk  30107  ordtrestNEW  33882  ordtrest2NEWlem  33883  omsval  34275  orrvcval4  34446  orrvcoel  34447  orrvccel  34448  funray  36122  fvray  36123  itg2addnclem2  37659  cntotbnd  37783  lcfr  41568  hlhilocv  41944  pellfundval  42868  elmnc  43125  rfovd  43991  fsovd  43998  fsovcnvlem  44003  ntrneibex  44063  dvnprodlem2  45903  dvnprodlem3  45904  dvnprod  45905  fvmptrab  47242  rmsuppss  48215  scmsuppss  48216  dmatALTbas  48247