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

Theorem chvar 1968
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 199 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 1957 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1557 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   F/wnf 1553
This theorem is referenced by:  chvarv  1969  csbhypf  3278  axrep2  4314  axrep3  4315  opelopabsb  4457  tfindes  4834  findes  4867  dfoprab4f  6397  dom2lem  7139  zfcndrep  8481  pwfseqlem4a  8528  pwfseqlem4  8529  uzind4s  10528  seqof2  11373  gsumcom2  15541  ptcldmpt  17638  elmptrab  17851  isfildlem  17881  dvmptfsum  19851  dvfsumlem2  19903  fmptcof2  24068  measiun  24564  lgamgulmlem2  24806  setinds  25397  wfisg  25476  frinsg  25512  fdc1  26441  fphpd  26868  monotuz  26995  monotoddzz  26997  oddcomabszz  26998  setindtrs  27087  flcidc  27347  fmul01  27677  fmuldfeq  27680  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climmulf  27697  climexp  27698  climsuse  27701  climrecf  27702  climinff  27704  stoweidlem3  27719  stoweidlem34  27750  stoweidlem42  27758  stoweidlem48  27764  bnj849  29233  bnj1014  29268  bnj1384  29338  bnj1489  29362  bnj1497  29366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator