MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chvar Structured version   Unicode version

Theorem chvar 2018
Description: Implicit substitution of  y for  x into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
chvar.1  |-  F/ x ps
chvar.2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
chvar.3  |-  ph
Assertion
Ref Expression
chvar  |-  ps

Proof of Theorem chvar
StepHypRef Expression
1 chvar.1 . . 3  |-  F/ x ps
2 chvar.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32biimpd 207 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 2011 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1625 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622
This theorem is referenced by:  chvarv  2019  csbhypf  3439  axrep2  4552  axrep3  4553  opelopabsb  4746  tfindes  6670  findes  6703  dfoprab4f  6831  dom2lem  7548  zfcndrep  8981  pwfseqlem4a  9028  pwfseqlem4  9029  uzind4s  11142  seqof2  12147  gsumcom2  17199  mdetralt2  19278  mdetunilem2  19282  ptcldmpt  20281  elmptrab  20494  isfildlem  20524  dvmptfsum  22542  dvfsumlem2  22594  fmptcof2  27724  aciunf1lem  27729  esum2dlem  28321  measiun  28426  lgamgulmlem2  28836  setinds  29450  wfisg  29529  frinsg  29565  ptrest  30288  fdc1  30479  fphpd  30989  monotuz  31116  monotoddzz  31118  oddcomabszz  31119  setindtrs  31206  flcidc  31364  binomcxplemnotnn0  31502  fsumclf  31806  fsumsplitf  31807  fsummulc1f  31808  fsumnncl  31811  fmul01  31813  fmuldfeq  31816  fmul01lt1lem1  31817  fmul01lt1lem2  31818  fproddivf  31827  fprodsplitf  31828  fprodexp  31839  fprodabs2  31841  climmulf  31849  climexp  31850  climsuse  31853  climrecf  31854  climinff  31856  climaddf  31860  mullimc  31861  neglimc  31892  addlimc  31893  0ellimcdiv  31894  fprodcncf  31943  dvmptmulf  31973  dvnmptdivc  31974  dvnmul  31979  dvmptfprod  31981  stoweidlem3  32024  stoweidlem34  32055  stoweidlem42  32063  stoweidlem48  32069  fourierdlem112  32240  bnj849  34384  bnj1014  34419  bnj1384  34489  bnj1489  34513  bnj1497  34517  fsumshftd  35079  fsumshftdOLD  35080
  Copyright terms: Public domain W3C validator