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

Theorem nfov 6904
Description: Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
Hypotheses
Ref Expression
nfov.1 𝑥𝐴
nfov.2 𝑥𝐹
nfov.3 𝑥𝐵
Assertion
Ref Expression
nfov 𝑥(𝐴𝐹𝐵)

Proof of Theorem nfov
StepHypRef Expression
1 nfov.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfov.2 . . . 4 𝑥𝐹
43a1i 11 . . 3 (⊤ → 𝑥𝐹)
5 nfov.3 . . . 4 𝑥𝐵
65a1i 11 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfovd 6903 . 2 (⊤ → 𝑥(𝐴𝐹𝐵))
87mptru 1645 1 𝑥(𝐴𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1638  wnfc 2935  (class class class)co 6874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6064  df-fv 6109  df-ov 6877
This theorem is referenced by:  csbov123  6915  ovmpt2s  7014  ov2gf  7015  ovmpt2dxf  7016  ovmpt2dv2  7024  ov3  7027  nfof  7132  offval2f  7139  offval2  7144  ofmpteq  7146  oawordeulem  7871  nnawordex  7954  pwfseqlem2  9766  pwfseqlem4a  9768  pwfseqlem4  9769  nfseq  13034  rlim2  14450  fsumadd  14693  fsummulc2  14738  fsumrlim  14765  fprodmul  14911  fproddiv  14912  fproddivf  14938  pcmpt  15813  pcmptdvds  15815  prdsdsval2  16349  gsum2d2  18574  gsumcom2  18575  prdsgsum  18578  dprd2d2  18645  gsumdixp  18811  evlslem4  19716  gsumply1eq  19883  madugsum  20660  cayleyhamilton1  20910  fiuncmp  21421  cnmpt2t  21690  cnmptcom  21695  cnmpt2k  21705  fsumcn  22886  ovoliunlem3  23485  isibl2  23747  nfitg1  23754  nfitg  23755  cbvitg  23756  itgfsum  23807  limciun  23872  dvmptfsum  23952  dvlipcn  23971  lhop2  23992  dvfsumabs  24000  dvfsumlem1  24003  dvfsumlem4  24006  dvfsum2  24011  itgparts  24024  itgsubstlem  24025  itgsubst  24026  elplyd  24172  coeeq2  24212  leibpi  24883  rlimcnp  24906  o1cxp  24915  dchrisumlem2  25393  dchrisumlem3  25394  numclwwlk1lem2OLD  27540  numclwlk2lem2f1o  27559  numclwlk2lem2f1oOLD  27566  cnlnadjlem5  29258  iundisjf  29727  gsumvsca1  30107  gsumvsca2  30108  nfesum1  30427  nfesum2  30428  esum2d  30480  nffrecs  32099  cnfinltrel  33557  ptrest  33721  sdclem1  33850  totbndbnd  33899  cdleme26ee  36141  cdleme31se2  36164  cdleme42b  36259  cdlemk11t  36727  dvdsrabdioph  37876  binomcxplemdvbinom  39052  binomcxplemdvsum  39054  binomcxplemnotnn0  39055  rfcnpre1  39672  rfcnpre2  39684  iunmapss  39894  ssmapsn  39895  infrpgernmpt  40174  fsummulc1f  40282  mulc1cncfg  40301  expcnfg  40303  fprodexp  40306  climmulf  40316  climexp  40317  climsuse  40320  climrecf  40321  climaddf  40327  mullimc  40328  idlimc  40338  limcperiod  40340  addlimc  40360  0ellimcdiv  40361  climsubmpt  40372  fnlimabslt  40391  climuz  40456  limsupgt  40490  liminflt  40517  cncfshift  40567  dvmptmulf  40632  dvnmul  40638  dvmptfprodlem  40639  dvmptfprod  40640  stoweidlem23  40719  stoweidlem28  40724  stoweidlem36  40732  wallispilem5  40765  stirlinglem15  40784  fourierdlem20  40823  fourierdlem31  40834  fourierdlem68  40870  fourierdlem80  40882  fourierdlem86  40888  fourierdlem103  40905  fourierdlem104  40906  fourierdlem112  40914  fourierdlem115  40917  fourierd  40918  fourierclimd  40919  etransclem2  40932  sge0ltfirp  41096  sge0xaddlem2  41130  sge0xadd  41131  hoimbl2  41361  vonhoire  41368  vonioo  41378  vonicc  41381  vonn0ioo2  41386  vonn0icc2  41388  smflimlem6  41466  ovmpt2rdxf  42685  aacllem  43118
  Copyright terms: Public domain W3C validator