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

Theorem sbceq1d 3592
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 3589 . 2 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
31, 2syl 17 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐵 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  [wsbc 3587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767  df-sbc 3588
This theorem is referenced by:  sbceq1dd  3593  sbcnestgf  4140  ralrnmpt  6513  tfindes  7213  findes  7247  findcard2  8360  ac6sfi  8364  indexfi  8434  ac6num  9507  nn1suc  11247  uzind4s  11955  uzind4s2  11956  fzrevral  12632  fzshftral  12635  fi1uzind  13481  wrdind  13685  wrd2ind  13686  cjth  14051  prmind2  15605  isprs  17138  isdrs  17142  joinlem  17219  meetlem  17233  istos  17243  isdlat  17401  gsumvalx  17478  mrcmndind  17574  issrg  18715  islmod  19077  quotval  24267  nn0min  29907  bnj944  31346  sdclem2  33868  fdc  33871  hdmap1ffval  37603  hdmap1fval  37604  rexrabdioph  37882  2nn0ind  38034  zindbi  38035  iotasbcq  39162
  Copyright terms: Public domain W3C validator