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

Theorem chvar 1939
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 198 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 1928 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1538 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1534
This theorem is referenced by:  csbhypf  3129  axrep2  4149  axrep3  4150  opelopabsb  4291  tfindes  4669  findes  4702  dfoprab4f  6194  dom2lem  6917  zfcndrep  8252  pwfseqlem4a  8299  pwfseqlem4  8300  uzind4s  10294  gsumcom2  15242  ptcldmpt  17324  elmptrab  17538  isfildlem  17568  dvmptfsum  19338  dvfsumlem2  19390  esumcvg  23469  measiun  23560  setinds  24205  wfisg  24280  frinsg  24316  fdc1  26559  fphpd  27002  monotuz  27129  monotoddzz  27131  oddcomabszz  27132  setindtrs  27221  flcidc  27482  climexp  27834  climsuse  27837  climinff  27840  bnj849  29273  bnj1014  29308  bnj1384  29378  bnj1489  29402  bnj1497  29406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator