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

Theorem nfov 6222
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
StepHypRef Expression
1 nfov.1 . . . 4  |-  F/_ x A
21a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
3 nfov.2 . . . 4  |-  F/_ x F
43a1i 11 . . 3  |-  ( T. 
->  F/_ x F )
5 nfov.3 . . . 4  |-  F/_ x B
65a1i 11 . . 3  |-  ( T. 
->  F/_ x B )
72, 4, 6nfovd 6221 . 2  |-  ( T. 
->  F/_ x ( A F B ) )
87trud 1408 1  |-  F/_ x
( A F B )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1400   F/_wnfc 2530  (class class class)co 6196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  csbov123  6230  ovmpt2s  6325  ov2gf  6326  ovmpt2dxf  6327  ovmpt2dv2  6335  ov3  6338  offval2  6455  ofmpteq  6457  oawordeulem  7121  nnawordex  7204  pwfseqlem2  8948  pwfseqlem4a  8950  pwfseqlem4  8951  nfseq  12020  rlim2  13321  fsumadd  13563  fsummulc2  13601  fsumrlim  13627  fprodmul  13767  fproddiv  13768  pcmpt  14413  pcmptdvds  14415  prdsdsval2  14891  gsum2d2  17116  gsumcom2  17117  prdsgsum  17120  prdsgsumOLD  17121  dprd2d2  17206  gsumdixpOLD  17370  gsumdixp  17371  evlslem4OLD  18286  evlslem4  18287  gsumply1eq  18460  madugsum  19230  cayleyhamilton1  19478  fiuncmp  19990  cnmpt2t  20259  cnmptcom  20264  cnmpt2k  20274  fsumcn  21459  ovoliunlem3  22000  isibl2  22258  nfitg1  22265  nfitg  22266  cbvitg  22267  itgfsum  22318  limciun  22383  dvmptfsum  22461  dvlipcn  22480  lhop2  22501  dvfsumabs  22509  dvfsumlem1  22512  dvfsumlem4  22515  dvfsum2  22520  itgparts  22533  itgsubstlem  22534  itgsubst  22535  elplyd  22684  coeeq2  22724  leibpi  23389  rlimcnp  23412  o1cxp  23421  dchrisumlem2  23792  dchrisumlem3  23793  cnlnadjlem5  27106  iundisjf  27578  offval2f  27652  gsumvsca1  27927  gsumvsca2  27928  nfesum1  28188  nfesum2  28189  esum2d  28241  ptrest  30213  sdclem1  30402  totbndbnd  30451  dvdsrabdioph  30909  binomcxplemdvbinom  31426  binomcxplemdvsum  31428  binomcxplemnotnn0  31429  rfcnpre1  31561  rfcnpre2  31573  fsummulc1f  31735  mulc1cncfg  31749  expcnfg  31752  fproddivf  31754  fprodexp  31766  climmulf  31776  climexp  31777  climsuse  31780  climrecf  31781  climaddf  31787  mullimc  31788  idlimc  31798  limcperiod  31800  addlimc  31820  0ellimcdiv  31821  cncfshift  31842  dvmptmulf  31900  dvnmul  31906  dvmptfprodlem  31907  dvmptfprod  31908  stoweidlem23  31971  stoweidlem28  31976  stoweidlem36  31984  wallispilem5  32017  stirlinglem15  32036  fourierdlem20  32075  fourierdlem31  32086  fourierdlem68  32123  fourierdlem80  32135  fourierdlem86  32141  fourierdlem103  32158  fourierdlem104  32159  fourierdlem112  32167  fourierdlem115  32170  fourierd  32171  fourierclimd  32172  etransclem2  32185  ovmpt2rdxf  33128  aacllem  33550  cdleme26ee  36499  cdleme31se2  36522  cdleme42b  36617  cdlemk11t  37085
  Copyright terms: Public domain W3C validator