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

Theorem sbceq1d 3638
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 3635 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  [wsbc 3633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802  df-sbc 3634
This theorem is referenced by:  sbceq1dd  3639  sbcnestgf  4192  ralrnmpt  6590  tfindes  7292  findes  7326  findcard2  8439  ac6sfi  8443  indexfi  8513  ac6num  9586  nn1suc  11326  uzind4s  11966  uzind4s2  11967  fzrevral  12648  fzshftral  12651  fi1uzind  13496  wrdind  13700  wrd2ind  13701  cjth  14066  prmind2  15616  isprs  17135  isdrs  17139  joinlem  17216  meetlem  17230  istos  17240  isdlat  17398  gsumvalx  17475  mrcmndind  17571  issrg  18709  islmod  19071  quotval  24261  nn0min  29894  bnj944  31331  sdclem2  33849  fdc  33852  hdmap1ffval  37576  hdmap1fval  37577  rexrabdioph  37860  2nn0ind  38011  zindbi  38012  iotasbcq  39137
  Copyright terms: Public domain W3C validator