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

Theorem sbceq1d 3716
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 3713 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  [wsbc 3711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-sbc 3712
This theorem is referenced by:  sbceq1dd  3717  sbcnestgfw  4349  sbcnestgf  4354  ralrnmptw  6952  ralrnmpt  6954  tfindes  7684  findes  7723  findcard2  8909  findcard2OLD  8986  ac6sfi  8988  indexfi  9057  ac6num  10166  nn1suc  11925  uzind4s  12577  uzind4s2  12578  fzrevral  13270  fzshftral  13273  fi1uzind  14139  wrdind  14363  wrd2ind  14364  cjth  14742  prmind2  16318  isprs  17930  isdrs  17934  joinlem  18016  meetlem  18030  istos  18051  isdlat  18155  gsumvalx  18275  mndind  18381  issrg  19658  islmod  20042  quotval  25357  nn0min  31036  wrdt2ind  31127  bnj944  32818  frpoins3xpg  33714  frpoins3xp3g  33715  sdclem2  35827  fdc  35830  hdmap1ffval  39736  hdmap1fval  39737  rexrabdioph  40532  2nn0ind  40683  zindbi  40684  iotasbcq  41944  prproropreud  44849
  Copyright terms: Public domain W3C validator