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

Theorem chvar 1962
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 1955 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1598 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-12 1797  ax-13 1948
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by:  chvarv  1963  csbhypf  3304  axrep2  4402  axrep3  4403  opelopabsb  4597  tfindes  6472  findes  6505  dfoprab4f  6631  dom2lem  7345  zfcndrep  8777  pwfseqlem4a  8824  pwfseqlem4  8825  uzind4s  10910  seqof2  11860  gsumcom2  16457  mdetralt2  18374  mdetunilem2  18378  ptcldmpt  19146  elmptrab  19359  isfildlem  19389  dvmptfsum  21406  dvfsumlem2  21458  fmptcof2  25914  measiun  26568  lgamgulmlem2  26946  setinds  27520  wfisg  27599  frinsg  27635  ptrest  28350  fdc1  28567  sbcalf  28845  sbcexf  28846  fphpd  29080  monotuz  29207  monotoddzz  29209  oddcomabszz  29210  setindtrs  29299  flcidc  29456  fmul01  29686  fmuldfeq  29689  fmul01lt1lem1  29690  fmul01lt1lem2  29691  climmulf  29702  climexp  29703  climsuse  29706  climrecf  29707  climinff  29709  stoweidlem3  29723  stoweidlem34  29754  stoweidlem42  29762  stoweidlem48  29768  bnj849  31752  bnj1014  31787  bnj1384  31857  bnj1489  31881  bnj1497  31885
  Copyright terms: Public domain W3C validator