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: Version of chvar 2406 with a disjoint variable condition, which does not require ax-13 2383. (Contributed 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 231 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
41, 3spimfv 2233 . 2 (∀𝑥𝜑𝜓)
5 chvarfv.2 . 2 𝜑
64, 5mpg 1791 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2169
This theorem depends on definitions:  df-bi 209  df-ex 1774  df-nf 1778
This theorem is referenced by:  csbhypf  3909  axrep2  5184  axrep3  5185  opelopabsb  5408  isso2i  5501  wfisg  6176  tfindes  7569  findes  7604  dfoprab4f  7746  dom2lem  8541  pwfseqlem4a  10075  pwfseqlem4  10076  uzind4s  12300  seqof2  13420  fsumsplitf  15090  fproddivf  15333  fprodsplitf  15334  gsumcom2  19087  mdetralt2  21210  mdetunilem2  21214  ptcldmpt  22214  elmptrab  22427  isfildlem  22457  dvmptfsum  24564  dvfsumlem2  24616  lgamgulmlem2  25599  fmptcof2  30394  aciunf1lem  30399  fsumiunle  30538  esum2dlem  31344  fiunelros  31426  measiun  31470  bnj849  32190  bnj1014  32226  bnj1384  32297  bnj1489  32321  bnj1497  32325  setinds  33016  frpoinsg  33074  frinsg  33080  finxpreclem6  34669  ptrest  34883  poimirlem24  34908  poimirlem25  34909  poimirlem26  34910  fdc1  35013  fsumshftd  36080  fphpd  39403  monotuz  39528  monotoddzz  39530  oddcomabszz  39531  setindtrs  39612  flcidc  39764  binomcxplemnotnn0  40678  fiiuncl  41317  disjf1  41432  disjinfi  41443  supxrleubrnmptf  41716  monoordxr  41748  monoord2xr  41750  fsumclf  41839  fsummulc1f  41840  fsumnncl  41841  fsumf1of  41844  fsumiunss  41845  fsumreclf  41846  fsumlessf  41847  fsumsermpt  41849  fmul01  41850  fmuldfeq  41853  fmul01lt1lem1  41854  fmul01lt1lem2  41855  fprodexp  41864  fprodabs2  41865  climmulf  41874  climexp  41875  climsuse  41878  climrecf  41879  climinff  41881  climaddf  41885  mullimc  41886  neglimc  41917  addlimc  41918  0ellimcdiv  41919  climsubmpt  41930  climreclf  41934  climeldmeqmpt  41938  climfveqmpt  41941  fnlimfvre  41944  climfveqf  41950  climfveqmpt3  41952  climeldmeqf  41953  climeqf  41958  climeldmeqmpt3  41959  climinf2  41977  climinf2mpt  41984  climinfmpt  41985  limsupequz  41993  limsupequzmptf  42001  fprodcncf  42173  dvmptmulf  42211  dvnmptdivc  42212  dvnmul  42217  dvmptfprod  42219  stoweidlem3  42278  stoweidlem34  42309  stoweidlem42  42317  stoweidlem48  42323  fourierdlem112  42493  sge0lempt  42682  sge0iunmptlemfi  42685  sge0iunmptlemre  42687  sge0iunmpt  42690  sge0ltfirpmpt2  42698  sge0isummpt2  42704  sge0xaddlem2  42706  sge0xadd  42707  meadjiun  42738  voliunsge0lem  42744  meaiunincf  42755  meaiuninc3  42757  meaiininc  42759  hoimbl2  42937  vonhoire  42944  vonn0ioo2  42962  vonn0icc2  42964  salpreimagtlt  42997
  Copyright terms: Public domain W3C validator