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

Theorem nfov 6105
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 6104 . 2  |-  ( T. 
->  F/_ x ( A F B ) )
87trud 1373 1  |-  F/_ x
( A F B )
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1365   F/_wnfc 2558  (class class class)co 6082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-iota 5371  df-fv 5416  df-ov 6085
This theorem is referenced by:  csbov123  6113  csbovgOLD  6115  ovmpt2s  6205  ov2gf  6206  ovmpt2dxf  6207  ovmpt2dv2  6215  ov3  6218  offval2  6327  ofmpteq  6329  oawordeulem  6983  nnawordex  7066  pwfseqlem2  8816  pwfseqlem4a  8818  pwfseqlem4  8819  nfseq  11802  rlim2  12960  fsumadd  13201  fsummulc2  13236  fsumrlim  13259  pcmpt  13939  pcmptdvds  13941  prdsdsval2  14407  gsum2d2  16442  gsumcom2  16443  prdsgsum  16447  prdsgsumOLD  16448  dprd2d2  16519  gsumdixpOLD  16637  gsumdixp  16638  evlslem4OLD  17520  evlslem4  17521  madugsum  18293  fiuncmp  18851  cnmpt2t  19090  cnmptcom  19095  cnmpt2k  19105  fsumcn  20290  ovoliunlem3  20831  isibl2  21088  nfitg1  21095  nfitg  21096  cbvitg  21097  itgfsum  21148  limciun  21213  dvmptfsum  21291  dvlipcn  21310  lhop2  21331  dvfsumabs  21339  dvfsumlem1  21342  dvfsumlem4  21345  dvfsum2  21350  itgparts  21363  itgsubstlem  21364  itgsubst  21365  elplyd  21557  coeeq2  21597  leibpi  22224  rlimcnp  22246  o1cxp  22255  dchrisumlem2  22626  dchrisumlem3  22627  cnlnadjlem5  25300  iundisjf  25757  offval2f  25809  gsumvsca1  26106  gsumvsca2  26107  nfesum1  26352  fprodmul  27320  fproddiv  27321  ptrest  28271  sdclem1  28485  totbndbnd  28534  dvdsrabdioph  28995  rfcnpre1  29588  rfcnpre2  29600  mulc1cncfg  29618  expcnfg  29621  climmulf  29625  climexp  29626  climsuse  29629  climrecf  29630  stoweidlem23  29666  stoweidlem28  29671  stoweidlem36  29679  wallispilem5  29712  stirlinglem15  29731  ovmpt2rdxf  30576  cdleme26ee  33617  cdleme31se2  33640  cdleme42b  33735  cdlemk11t  34203
  Copyright terms: Public domain W3C validator