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

Theorem nfov 5881
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 10 . . 3  |-  (  T. 
->  F/_ x A )
3 nfov.2 . . . 4  |-  F/_ x F
43a1i 10 . . 3  |-  (  T. 
->  F/_ x F )
5 nfov.3 . . . 4  |-  F/_ x B
65a1i 10 . . 3  |-  (  T. 
->  F/_ x B )
72, 4, 6nfovd 5880 . 2  |-  (  T. 
->  F/_ x ( A F B ) )
87trud 1314 1  |-  F/_ x
( A F B )
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/_wnfc 2406  (class class class)co 5858
This theorem is referenced by:  csbovg  5889  ovmpt2s  5971  ov2gf  5972  ovmpt2dxf  5973  ovmpt2dv2  5981  ov3  5984  nfof  6083  offval2  6095  oawordeulem  6552  nnawordex  6635  pwfseqlem2  8281  pwfseqlem4a  8283  pwfseqlem4  8284  nfseq  11056  rlim2  11970  fsumadd  12211  fsummulc2  12246  fsumrlim  12269  pcmpt  12940  pcmptdvds  12942  prdsdsval2  13383  gsum2d2  15225  gsumcom2  15226  prdsgsum  15229  dprd2d2  15279  gsumdixp  15392  evlslem4  16245  fiuncmp  17131  cnmpt2t  17367  cnmptcom  17372  cnmpt2k  17382  fsumcn  18374  ovoliunlem3  18863  isibl2  19121  nfitg1  19128  nfitg  19129  cbvitg  19130  itgfsum  19181  limciun  19244  dvmptfsum  19322  dvlipcn  19341  lhop2  19362  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem4  19376  dvfsum2  19381  itgparts  19394  itgsubstlem  19395  itgsubst  19396  elplyd  19584  coeeq2  19624  leibpi  20238  rlimcnp  20260  o1cxp  20269  dchrisumlem2  20639  dchrisumlem3  20640  cnlnadjlem5  22651  offval2f  23233  iundisjf  23365  dya2iocrrnval  23582  fprodadd  25352  fprodsub  25379  sdclem1  26453  totbndbnd  26513  ofmpteq  26797  dvdsrabdioph  26891  rfcnpre1  27690  rfcnpre2  27702  mulc1cncfg  27721  expcnfg  27726  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  stoweidlem23  27772  stoweidlem28  27777  stoweidlem36  27785  wallispilem5  27818  stirlinglem15  27837  cdleme26ee  30549  cdleme31se2  30572  cdleme42b  30667  cdlemk11t  31135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator