Theorem nfov 6676

Description: Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)

Hypotheses

Ref	Expression
nfov.1	|- F/_ x A
nfov.2	|- F/_ x F
nfov.3	|- F/_ x B

Assertion

Ref	Expression
nfov	|- F/_ x ( A F B )

Proof of Theorem nfov

Step	Hyp	Ref	Expression
1		nfov.1	. . . 4 |- F/_ x A
2	1	a1i 11	. . 3 |- ( T. -> F/_ x A )
3		nfov.2	. . . 4 |- F/_ x F
4	3	a1i 11	. . 3 |- ( T. -> F/_ x F )
5		nfov.3	. . . 4 |- F/_ x B
6	5	a1i 11	. . 3 |- ( T. -> F/_ x B )
7	2, 4, 6	nfovd 6675	. 2 |- ( T. -> F/_ x ( A F B ) )
8	7	trud 1493	1 |- F/_ x ( A F B )

Syntax hints:   T. wtru 1484   F/_wnfc 2751  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  csbov123  6687  ovmpt2s  6784  ov2gf  6785  ovmpt2dxf  6786  ovmpt2dv2  6794  ov3  6797  offval2f  6909  offval2  6914  ofmpteq  6916  oawordeulem  7634  nnawordex  7717  pwfseqlem2  9481  pwfseqlem4a  9483  pwfseqlem4  9484  nfseq  12811  rlim2  14227  fsumadd  14470  fsummulc2  14516  fsumrlim  14543  fprodmul  14690  fproddiv  14691  fproddivf  14718  pcmpt  15596  pcmptdvds  15598  prdsdsval2  16144  gsum2d2  18373  gsumcom2  18374  prdsgsum  18377  dprd2d2  18443  gsumdixp  18609  evlslem4  19508  gsumply1eq  19675  madugsum  20449  cayleyhamilton1  20697  fiuncmp  21207  cnmpt2t  21476  cnmptcom  21481  cnmpt2k  21491  fsumcn  22673  ovoliunlem3  23272  isibl2  23533  nfitg1  23540  nfitg  23541  cbvitg  23542  itgfsum  23593  limciun  23658  dvmptfsum  23738  dvlipcn  23757  lhop2  23778  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem4  23792  dvfsum2  23797  itgparts  23810  itgsubstlem  23811  itgsubst  23812  elplyd  23958  coeeq2  23998  leibpi  24669  rlimcnp  24692  o1cxp  24701  dchrisumlem2  25179  dchrisumlem3  25180  numclwlk1lem2  27230  numclwlk2lem2f1o  27238  cnlnadjlem5  28930  iundisjf  29402  gsumvsca1  29782  gsumvsca2  29783  nfesum1  30102  nfesum2  30103  esum2d  30155  ptrest  33408  sdclem1  33539  totbndbnd  33588  cdleme26ee  35648  cdleme31se2  35671  cdleme42b  35766  cdlemk11t  36234  dvdsrabdioph  37374  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  rfcnpre1  39178  rfcnpre2  39190  iunmapss  39407  ssmapsn  39408  infrpgernmpt  39695  fsummulc1f  39802  mulc1cncfg  39821  expcnfg  39823  fprodexp  39826  climmulf  39836  climexp  39837  climsuse  39840  climrecf  39841  climaddf  39847  mullimc  39848  idlimc  39858  limcperiod  39860  addlimc  39880  0ellimcdiv  39881  climsubmpt  39892  fnlimabslt  39911  climuz  39976  limsupgt  40010  liminflt  40037  cncfshift  40087  dvmptmulf  40152  dvnmul  40158  dvmptfprodlem  40159  dvmptfprod  40160  stoweidlem23  40240  stoweidlem28  40245  stoweidlem36  40253  wallispilem5  40286  stirlinglem15  40305  fourierdlem20  40344  fourierdlem31  40355  fourierdlem68  40391  fourierdlem80  40403  fourierdlem86  40409  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem115  40438  fourierd  40439  fourierclimd  40440  etransclem2  40453  sge0ltfirp  40617  sge0xaddlem2  40651  sge0xadd  40652  hoimbl2  40879  vonhoire  40886  vonioo  40896  vonicc  40899  vonn0ioo2  40904  vonn0icc2  40906  smflimlem6  40984  ovmpt2rdxf  42117  aacllem  42547