Theorem rabeq 3397

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2143, ax-11 2159, ax-12 2176. (Revised by Gino Giotto, 20-Aug-2023.)

Assertion

Ref	Expression
rabeq	⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabeq

Step	Hyp	Ref	Expression
1		eleq2 2841	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	rabbidva2 3389	1 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  {crab 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080

This theorem is referenced by:  rabeqdv  3398  difeq1  4022  ineq1  4110  ifeq1  4425  ifeq2  4426  elfvmptrab  6788  supp0  7841  supeq2  8946  oieq2  9011  scott0  9349  mrcfval  16938  ipoval  17831  psgnfval  18696  dsmmelbas  20505  psrval  20678  ltbval  20804  opsrval  20807  m1detdiag  21298  isptfin  22217  islocfin  22218  kqval  22427  incistruhgr  26972  uvtx0  27284  vtxdg0e  27364  1hevtxdg1  27396  hashecclwwlkn1  27962  umgrhashecclwwlk  27963  ordtrestNEW  31393  ordtrest2NEWlem  31394  omsval  31780  orrvcval4  31951  orrvcoel  31952  orrvccel  31953  funray  33992  fvray  33993  itg2addnclem2  35390  cntotbnd  35515  lcfr  39162  hlhilocv  39534  pellfundval  40195  elmnc  40454  rgspnval  40486  rfovd  41076  fsovd  41083  fsovcnvlem  41088  ntrneibex  41150  dvnprodlem1  42955  dvnprodlem2  42956  dvnprodlem3  42957  dvnprod  42958  fvmptrab  44217  rmsuppss  45140  mndpsuppss  45141  scmsuppss  45142  dmatALTbas  45176