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

Theorem chvarfv 2236
Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2395 with a disjoint variable condition, which does not require ax-13 2372. (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 2235 . 2 (∀𝑥𝜑𝜓)
5 chvarfv.2 . 2 𝜑
64, 5mpg 1801 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wnf 1787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173
This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788
This theorem is referenced by:  csbhypf  3857  axrep2  5208  axrep3  5209  isso2i  5529  frpoinsg  6231  wfisgOLD  6242  tfindes  7684  findes  7723  dfoprab4f  7869  dom2lem  8735  frinsg  9440  pwfseqlem4a  10348  pwfseqlem4  10349  uzind4s  12577  seqof2  13709  fsumclf  15378  fsumsplitf  15382  fproddivf  15625  fprodsplitf  15626  gsumcom2  19491  mdetralt2  21666  mdetunilem2  21670  ptcldmpt  22673  elmptrab  22886  isfildlem  22916  dvmptfsum  25044  dvfsumlem2  25096  lgamgulmlem2  26084  fmptcof2  30896  aciunf1lem  30901  fsumiunle  31045  esum2dlem  31960  fiunelros  32042  measiun  32086  bnj849  32805  bnj1014  32841  bnj1384  32912  bnj1489  32936  bnj1497  32940  setinds  33660  finxpreclem6  35494  ptrest  35703  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  fdc1  35831  fsumshftd  36893  fphpd  40554  monotuz  40679  monotoddzz  40681  oddcomabszz  40682  setindtrs  40763  flcidc  40915  binomcxplemnotnn0  41863  fiiuncl  42502  disjf1  42609  disjinfi  42620  supxrleubrnmptf  42881  monoordxr  42913  monoord2xr  42915  fsummulc1f  43002  fsumnncl  43003  fsumf1of  43005  fsumiunss  43006  fsumreclf  43007  fsumlessf  43008  fsumsermpt  43010  fmul01  43011  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fprodexp  43025  fprodabs2  43026  climmulf  43035  climexp  43036  climsuse  43039  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  neglimc  43078  addlimc  43079  0ellimcdiv  43080  climsubmpt  43091  climreclf  43095  climeldmeqmpt  43099  climfveqmpt  43102  fnlimfvre  43105  climfveqf  43111  climfveqmpt3  43113  climeldmeqf  43114  climeqf  43119  climeldmeqmpt3  43120  climinf2  43138  climinf2mpt  43145  climinfmpt  43146  limsupequz  43154  limsupequzmptf  43162  fprodcncf  43331  dvmptmulf  43368  dvnmptdivc  43369  dvnmul  43374  dvmptfprod  43376  stoweidlem3  43434  stoweidlem34  43465  stoweidlem42  43473  stoweidlem48  43479  fourierdlem112  43649  sge0lempt  43838  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isummpt2  43860  sge0xaddlem2  43862  sge0xadd  43863  meadjiun  43894  voliunsge0lem  43900  meaiunincf  43911  meaiuninc3  43913  meaiininc  43915  hoimbl2  44093  vonhoire  44100  vonn0ioo2  44118  vonn0icc2  44120  salpreimagtlt  44153
  Copyright terms: Public domain W3C validator