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 207 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 1961 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1594 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1954
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  chvarv  1969  csbhypf  3409  axrep2  4508  axrep3  4509  opelopabsb  4702  tfindes  6578  findes  6611  dfoprab4f  6737  dom2lem  7454  zfcndrep  8887  pwfseqlem4a  8934  pwfseqlem4  8935  uzind4s  11020  seqof2  11976  gsumcom2  16584  mdetralt2  18542  mdetunilem2  18546  ptcldmpt  19314  elmptrab  19527  isfildlem  19557  dvmptfsum  21575  dvfsumlem2  21627  fmptcof2  26125  measiun  26772  lgamgulmlem2  27155  setinds  27730  wfisg  27809  frinsg  27845  ptrest  28568  fdc1  28785  sbcalf  29063  sbcexf  29064  fphpd  29298  monotuz  29425  monotoddzz  29427  oddcomabszz  29428  setindtrs  29517  flcidc  29674  fmul01  29904  fmuldfeq  29907  fmul01lt1lem1  29908  fmul01lt1lem2  29909  climmulf  29920  climexp  29921  climsuse  29924  climrecf  29925  climinff  29927  stoweidlem3  29941  stoweidlem34  29972  stoweidlem42  29980  stoweidlem48  29986  bnj849  32231  bnj1014  32266  bnj1384  32336  bnj1489  32360  bnj1497  32364  fsumshftd  32921  fsumshftdOLD  32922
  Copyright terms: Public domain W3C validator