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

Theorem chvar 2107
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 212 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 2099 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1675 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   F/wnf 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-12 1937  ax-13 2092
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1668  df-nf 1672
This theorem is referenced by:  chvarv  2108  csbhypf  3350  axrep2  4489  axrep3  4490  opelopabsb  4684  wfisg  5394  tfindes  6677  findes  6711  dfoprab4f  6839  dom2lem  7596  zfcndrep  9026  pwfseqlem4a  9073  pwfseqlem4  9074  uzind4s  11209  seqof2  12265  fproddivf  14052  fprodsplitf  14053  gsumcom2  17618  mdetralt2  19645  mdetunilem2  19649  ptcldmpt  20640  elmptrab  20853  isfildlem  20883  dvmptfsum  22939  dvfsumlem2  22991  lgamgulmlem2  23967  fmptcof2  28267  aciunf1lem  28272  esum2dlem  28920  fiunelros  29003  measiun  29047  bnj849  29742  bnj1014  29777  bnj1384  29847  bnj1489  29871  bnj1497  29875  setinds  30430  frinsg  30489  finxpreclem6  31790  ptrest  31941  poimirlem24  31966  poimirlem25  31967  poimirlem26  31968  fdc1  32077  fsumshftd  32525  fsumshftdOLD  32526  fphpd  35661  monotuz  35791  monotoddzz  35793  oddcomabszz  35794  setindtrs  35882  flcidc  36042  binomcxplemnotnn0  36706  fiiuncl  37401  disjf1  37467  disjinfi  37478  fsumclf  37686  fsumsplitf  37687  fsummulc1f  37688  fsumnncl  37691  fsumf1of  37694  fsumiunss  37695  fsumreclf  37696  fsumlessf  37697  fsumsermpt  37699  fmul01  37700  fmuldfeq  37703  fmul01lt1lem1  37704  fmul01lt1lem2  37705  fprodexp  37716  fprodabs2  37717  climmulf  37724  climexp  37725  climsuse  37729  climrecf  37730  climinff  37732  climinffOLD  37733  climaddf  37737  mullimc  37738  neglimc  37770  addlimc  37771  0ellimcdiv  37772  fprodcncf  37821  dvmptmulf  37854  dvnmptdivc  37855  dvnmul  37860  dvmptfprod  37862  stoweidlem3  37920  stoweidlem34  37952  stoweidlem42  37960  stoweidlem48  37966  fourierdlem112  38139  sge0lempt  38311  sge0iunmptlemfi  38314  sge0iunmptlemre  38316  sge0iunmpt  38319  sge0ltfirpmpt2  38327  sge0isummpt2  38333  sge0xaddlem2  38335  sge0xadd  38336  meadjiun  38365  voliunsge0lem  38371
  Copyright terms: Public domain W3C validator