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

Theorem sbceq1d 3422
Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)
Hypothesis
Ref Expression
sbceq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
sbceq1d (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))

Proof of Theorem sbceq1d
StepHypRef Expression
1 sbceq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 dfsbcq 3419 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  [wsbc 3417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617  df-sbc 3418
This theorem is referenced by:  sbceq1dd  3423  sbcnestgf  3967  ralrnmpt  6324  tfindes  7009  findes  7043  findcard2  8144  ac6sfi  8148  indexfi  8218  ac6num  9245  nn1suc  10985  uzind4s  11692  uzind4s2  11693  fzrevral  12366  fzshftral  12369  fi1uzind  13218  fi1uzindOLD  13224  wrdind  13414  wrd2ind  13415  cjth  13777  prmind2  15322  isprs  16851  isdrs  16855  joinlem  16932  meetlem  16946  istos  16956  isdlat  17114  gsumvalx  17191  mrcmndind  17287  issrg  18428  islmod  18788  quotval  23951  nn0min  29405  bnj944  30713  sdclem2  33167  fdc  33170  hdmap1ffval  36562  hdmap1fval  36563  rexrabdioph  36835  2nn0ind  36987  zindbi  36988  iotasbcq  38117
  Copyright terms: Public domain W3C validator