Theorem nfov 6322

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

Step	Hyp	Ref	Expression
1		nfov.1	. . . 4
2	1	a1i 11	. . 3
3		nfov.2	. . . 4
4	3	a1i 11	. . 3
5		nfov.3	. . . 4
6	5	a1i 11	. . 3
7	2, 4, 6	nfovd 6321	. 2
8	7	trud 1404	1

Syntax hints:  wtru 1396  F/_wnfc 2605  (class class class)co 6296

This theorem is referenced by:  csbov123  6330  csbovgOLD  6332  ovmpt2s  6426  ov2gf  6427  ovmpt2dxf  6428  ovmpt2dv2  6436  ov3  6439  offval2  6556  ofmpteq  6558  oawordeulem  7222  nnawordex  7305  pwfseqlem2  9058  pwfseqlem4a  9060  pwfseqlem4  9061  nfseq  12117  rlim2  13319  fsumadd  13561  fsummulc2  13599  fsumrlim  13625  fprodmul  13765  fproddiv  13766  pcmpt  14411  pcmptdvds  14413  prdsdsval2  14881  gsum2d2  17002  gsumcom2  17003  prdsgsum  17007  prdsgsumOLD  17008  dprd2d2  17093  gsumdixpOLD  17257  gsumdixp  17258  evlslem4OLD  18173  evlslem4  18174  gsumply1eq  18347  madugsum  19145  cayleyhamilton1  19393  fiuncmp  19904  cnmpt2t  20174  cnmptcom  20179  cnmpt2k  20189  fsumcn  21374  ovoliunlem3  21915  isibl2  22173  nfitg1  22180  nfitg  22181  cbvitg  22182  itgfsum  22233  limciun  22298  dvmptfsum  22376  dvlipcn  22395  lhop2  22416  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem4  22430  dvfsum2  22435  itgparts  22448  itgsubstlem  22449  itgsubst  22450  elplyd  22599  coeeq2  22639  leibpi  23273  rlimcnp  23295  o1cxp  23304  dchrisumlem2  23675  dchrisumlem3  23676  cnlnadjlem5  26990  iundisjf  27448  offval2f  27506  gsumvsca1  27773  gsumvsca2  27774  nfesum1  28053  ptrest  30048  sdclem1  30236  totbndbnd  30285  dvdsrabdioph  30743  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  rfcnpre1  31394  rfcnpre2  31406  fsummulc1f  31569  mulc1cncfg  31583  expcnfg  31586  fproddivf  31588  fprodexp  31600  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climaddf  31621  mullimc  31622  idlimc  31632  limcperiod  31634  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  dvmptmulf  31734  dvnmul  31740  dvmptfprodlem  31741  dvmptfprod  31742  stoweidlem23  31805  stoweidlem28  31810  stoweidlem36  31818  wallispilem5  31851  stirlinglem15  31870  fourierdlem20  31909  fourierdlem31  31920  fourierdlem68  31957  fourierdlem80  31969  fourierdlem86  31975  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem115  32004  fourierd  32005  fourierclimd  32006  etransclem2  32019  ovmpt2rdxf  32928  aacllem  33216  cdleme26ee  36086  cdleme31se2  36109  cdleme42b  36204  cdlemk11t  36672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299