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

Theorem nfov 6114
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 6113 . 2  |-  ( T. 
->  F/_ x ( A F B ) )
87trud 1378 1  |-  F/_ x
( A F B )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1370   F/_wnfc 2566  (class class class)co 6091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094
This theorem is referenced by:  csbov123  6122  csbovgOLD  6124  ovmpt2s  6214  ov2gf  6215  ovmpt2dxf  6216  ovmpt2dv2  6224  ov3  6227  offval2  6336  ofmpteq  6338  oawordeulem  6993  nnawordex  7076  pwfseqlem2  8826  pwfseqlem4a  8828  pwfseqlem4  8829  nfseq  11816  rlim2  12974  fsumadd  13215  fsummulc2  13251  fsumrlim  13274  pcmpt  13954  pcmptdvds  13956  prdsdsval2  14422  gsum2d2  16466  gsumcom2  16467  prdsgsum  16471  prdsgsumOLD  16472  dprd2d2  16543  gsumdixpOLD  16700  gsumdixp  16701  evlslem4OLD  17590  evlslem4  17591  madugsum  18449  fiuncmp  19007  cnmpt2t  19246  cnmptcom  19251  cnmpt2k  19261  fsumcn  20446  ovoliunlem3  20987  isibl2  21244  nfitg1  21251  nfitg  21252  cbvitg  21253  itgfsum  21304  limciun  21369  dvmptfsum  21447  dvlipcn  21466  lhop2  21487  dvfsumabs  21495  dvfsumlem1  21498  dvfsumlem4  21501  dvfsum2  21506  itgparts  21519  itgsubstlem  21520  itgsubst  21521  elplyd  21670  coeeq2  21710  leibpi  22337  rlimcnp  22359  o1cxp  22368  dchrisumlem2  22739  dchrisumlem3  22740  cnlnadjlem5  25475  iundisjf  25931  offval2f  25983  gsumvsca1  26251  gsumvsca2  26252  nfesum1  26496  fprodmul  27471  fproddiv  27472  ptrest  28425  sdclem1  28639  totbndbnd  28688  dvdsrabdioph  29148  rfcnpre1  29741  rfcnpre2  29753  mulc1cncfg  29770  expcnfg  29773  climmulf  29777  climexp  29778  climsuse  29781  climrecf  29782  stoweidlem23  29818  stoweidlem28  29823  stoweidlem36  29831  wallispilem5  29864  stirlinglem15  29883  ovmpt2rdxf  30729  cdleme26ee  34004  cdleme31se2  34027  cdleme42b  34122  cdlemk11t  34590
  Copyright terms: Public domain W3C validator