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

Theorem chvar 1969
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 200 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 1958 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1558 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   F/wnf 1554
This theorem is referenced by:  chvarv  1970  csbhypf  3288  axrep2  4324  axrep3  4325  opelopabsb  4467  tfindes  4844  findes  4877  dfoprab4f  6407  dom2lem  7149  zfcndrep  8491  pwfseqlem4a  8538  pwfseqlem4  8539  uzind4s  10538  seqof2  11383  gsumcom2  15551  ptcldmpt  17648  elmptrab  17861  isfildlem  17891  dvmptfsum  19861  dvfsumlem2  19913  fmptcof2  24078  measiun  24574  lgamgulmlem2  24816  setinds  25407  wfisg  25486  frinsg  25522  fdc1  26452  fphpd  26879  monotuz  27006  monotoddzz  27008  oddcomabszz  27009  setindtrs  27098  flcidc  27358  fmul01  27688  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climmulf  27708  climexp  27709  climsuse  27712  climrecf  27713  climinff  27715  stoweidlem3  27730  stoweidlem34  27761  stoweidlem42  27769  stoweidlem48  27775  bnj849  29358  bnj1014  29393  bnj1384  29463  bnj1489  29487  bnj1497  29491
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator