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

Theorem chvar 2039
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 1955 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1554 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   F/wnf 1550
This theorem is referenced by:  csbhypf  3246  axrep2  4282  axrep3  4283  opelopabsb  4425  tfindes  4801  findes  4834  dfoprab4f  6364  dom2lem  7106  zfcndrep  8445  pwfseqlem4a  8492  pwfseqlem4  8493  uzind4s  10492  seqof2  11336  gsumcom2  15504  ptcldmpt  17599  elmptrab  17812  isfildlem  17842  dvmptfsum  19812  dvfsumlem2  19864  fmptcof2  24029  measiun  24525  lgamgulmlem2  24767  setinds  25348  wfisg  25423  frinsg  25459  fdc1  26340  fphpd  26767  monotuz  26894  monotoddzz  26896  oddcomabszz  26897  setindtrs  26986  flcidc  27247  fmul01  27577  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  stoweidlem3  27619  stoweidlem34  27650  stoweidlem42  27658  stoweidlem48  27664  bnj849  29002  bnj1014  29037  bnj1384  29107  bnj1489  29131  bnj1497  29135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator