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

Theorem chvarfv 2234
Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2394 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)
Hypotheses
Ref Expression
chvarfv.nf 𝑥𝜓
chvarfv.1 (𝑥 = 𝑦 → (𝜑𝜓))
chvarfv.2 𝜑
Assertion
Ref Expression
chvarfv 𝜓
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem chvarfv
StepHypRef Expression
1 chvarfv.nf . . 3 𝑥𝜓
2 chvarfv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32biimpd 228 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
41, 3spimfv 2233 . 2 (∀𝑥𝜑𝜓)
5 chvarfv.2 . 2 𝜑
64, 5mpg 1800 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787
This theorem is referenced by:  csbhypf  3889  axrep2  5250  axrep3  5251  isso2i  5585  frpoinsg  6302  wfisgOLD  6313  tfindes  7804  findes  7844  dfoprab4f  7993  dom2lem  8939  frinsg  9694  pwfseqlem4a  10604  pwfseqlem4  10605  uzind4s  12840  seqof2  13973  fsumclf  15630  fsumsplitf  15634  fproddivf  15877  fprodsplitf  15878  gsumcom2  19759  mdetralt2  21974  mdetunilem2  21978  ptcldmpt  22981  elmptrab  23194  isfildlem  23224  dvmptfsum  25355  dvfsumlem2  25407  lgamgulmlem2  26395  fmptcof2  31615  aciunf1lem  31620  fsumiunle  31767  esum2dlem  32731  fiunelros  32813  measiun  32857  bnj849  33577  bnj1014  33613  bnj1384  33684  bnj1489  33708  bnj1497  33712  setinds  34392  finxpreclem6  35896  ptrest  36106  poimirlem24  36131  poimirlem25  36132  poimirlem26  36133  fdc1  36234  fsumshftd  37443  fphpd  41168  monotuz  41294  monotoddzz  41296  oddcomabszz  41297  setindtrs  41378  flcidc  41530  binomcxplemnotnn0  42710  fiiuncl  43347  disjf1  43475  disjinfi  43486  supxrleubrnmptf  43760  monoordxr  43792  monoord2xr  43794  fsummulc1f  43886  fsumnncl  43887  fsumf1of  43889  fsumiunss  43890  fsumreclf  43891  fsumlessf  43892  fsumsermpt  43894  fmul01  43895  fmuldfeq  43898  fmul01lt1lem1  43899  fmul01lt1lem2  43900  fprodexp  43909  fprodabs2  43910  climmulf  43919  climexp  43920  climsuse  43923  climrecf  43924  climinff  43926  climaddf  43930  mullimc  43931  neglimc  43962  addlimc  43963  0ellimcdiv  43964  climsubmpt  43975  climreclf  43979  climeldmeqmpt  43983  climfveqmpt  43986  fnlimfvre  43989  climfveqf  43995  climfveqmpt3  43997  climeldmeqf  43998  climeqf  44003  climeldmeqmpt3  44004  climinf2  44022  climinf2mpt  44029  climinfmpt  44030  limsupequz  44038  limsupequzmptf  44046  fprodcncf  44215  dvmptmulf  44252  dvnmptdivc  44253  dvnmul  44258  dvmptfprod  44260  stoweidlem3  44318  stoweidlem34  44349  stoweidlem42  44357  stoweidlem48  44363  fourierdlem112  44533  sge0lempt  44725  sge0iunmptlemfi  44728  sge0iunmptlemre  44730  sge0iunmpt  44733  sge0ltfirpmpt2  44741  sge0isummpt2  44747  sge0xaddlem2  44749  sge0xadd  44750  meadjiun  44781  voliunsge0lem  44787  meaiunincf  44798  meaiuninc3  44800  meaiininc  44802  hoimbl2  44980  vonhoire  44987  vonn0ioo2  45005  vonn0icc2  45007  salpreimagtlt  45045
  Copyright terms: Public domain W3C validator