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

Theorem chvar 1926
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 1915 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1535 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1531
This theorem is referenced by:  csbhypf  3116  axrep2  4133  axrep3  4134  opelopabsb  4275  tfindes  4653  findes  4686  dfoprab4f  6178  dom2lem  6901  zfcndrep  8236  pwfseqlem4a  8283  pwfseqlem4  8284  uzind4s  10278  gsumcom2  15226  ptcldmpt  17308  elmptrab  17522  isfildlem  17552  dvmptfsum  19322  dvfsumlem2  19374  esumcvg  23454  measiun  23545  setinds  24134  wfisg  24209  frinsg  24245  fdc1  26456  fphpd  26899  monotuz  27026  monotoddzz  27028  oddcomabszz  27029  setindtrs  27118  flcidc  27379  climexp  27731  climsuse  27734  climinff  27737  bnj849  28957  bnj1014  28992  bnj1384  29062  bnj1489  29086  bnj1497  29090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator