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

Theorem chvar 2023
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 199 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 1948 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1554 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   F/wnf 1550
This theorem is referenced by:  csbhypf  3230  axrep2  4264  axrep3  4265  opelopabsb  4407  tfindes  4783  findes  4816  dfoprab4f  6345  dom2lem  7084  zfcndrep  8423  pwfseqlem4a  8470  pwfseqlem4  8471  uzind4s  10469  seqof2  11309  gsumcom2  15477  ptcldmpt  17568  elmptrab  17781  isfildlem  17811  dvmptfsum  19727  dvfsumlem2  19779  fmptcof2  23919  measiun  24367  lgamgulmlem2  24594  setinds  25159  wfisg  25234  frinsg  25270  fdc1  26142  fphpd  26569  monotuz  26696  monotoddzz  26698  oddcomabszz  26699  setindtrs  26788  flcidc  27049  fmul01  27379  fmuldfeq  27382  fmul01lt1lem1  27383  fmul01lt1lem2  27384  climmulf  27399  climexp  27400  climsuse  27403  climrecf  27404  climinff  27406  stoweidlem3  27421  stoweidlem34  27452  stoweidlem42  27460  stoweidlem48  27466  bnj849  28635  bnj1014  28670  bnj1384  28740  bnj1489  28764  bnj1497  28768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator