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

Theorem nfov 6104
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 6103 . 2  |-  (  T. 
->  F/_ x ( A F B ) )
87trud 1332 1  |-  F/_ x
( A F B )
Colors of variables: wff set class
Syntax hints:    T. wtru 1325   F/_wnfc 2559  (class class class)co 6081
This theorem is referenced by:  csbovg  6112  ovmpt2s  6197  ov2gf  6198  ovmpt2dxf  6199  ovmpt2dv2  6207  ov3  6210  offval2  6322  oawordeulem  6797  nnawordex  6880  pwfseqlem2  8534  pwfseqlem4a  8536  pwfseqlem4  8537  nfseq  11333  rlim2  12290  fsumadd  12532  fsummulc2  12567  fsumrlim  12590  pcmpt  13261  pcmptdvds  13263  prdsdsval2  13706  gsum2d2  15548  gsumcom2  15549  prdsgsum  15552  dprd2d2  15602  gsumdixp  15715  evlslem4  16564  fiuncmp  17467  cnmpt2t  17705  cnmptcom  17710  cnmpt2k  17720  fsumcn  18900  ovoliunlem3  19400  isibl2  19658  nfitg1  19665  nfitg  19666  cbvitg  19667  itgfsum  19718  limciun  19781  dvmptfsum  19859  dvlipcn  19878  lhop2  19899  dvfsumabs  19907  dvfsumlem1  19910  dvfsumlem4  19913  dvfsum2  19918  itgparts  19931  itgsubstlem  19932  itgsubst  19933  elplyd  20121  coeeq2  20161  leibpi  20782  rlimcnp  20804  o1cxp  20813  dchrisumlem2  21184  dchrisumlem3  21185  cnlnadjlem5  23574  iundisjf  24029  offval2f  24080  nfesum1  24437  fprodmul  25284  fproddiv  25285  sdclem1  26447  totbndbnd  26498  ofmpteq  26776  dvdsrabdioph  26870  rfcnpre1  27666  rfcnpre2  27678  mulc1cncfg  27697  expcnfg  27702  climmulf  27706  climexp  27707  climsuse  27710  climrecf  27711  stoweidlem23  27748  stoweidlem28  27753  stoweidlem36  27761  wallispilem5  27794  stirlinglem15  27813  cdleme26ee  31157  cdleme31se2  31180  cdleme42b  31275  cdlemk11t  31743
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084
  Copyright terms: Public domain W3C validator