Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabeq Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 eleq2 2841 . . 3 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21anbi1d 633 . 2 (𝐴 = 𝐵 → ((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜑)))
32rabbidva2 3389 1 (𝐴 = 𝐵 → {𝑥𝐴𝜑} = {𝑥𝐵𝜑})
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator