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

Theorem nfov 6063
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 6062 . 2  |-  (  T. 
->  F/_ x ( A F B ) )
87trud 1329 1  |-  F/_ x
( A F B )
Colors of variables: wff set class
Syntax hints:    T. wtru 1322   F/_wnfc 2527  (class class class)co 6040
This theorem is referenced by:  csbovg  6071  ovmpt2s  6156  ov2gf  6157  ovmpt2dxf  6158  ovmpt2dv2  6166  ov3  6169  offval2  6281  oawordeulem  6756  nnawordex  6839  pwfseqlem2  8490  pwfseqlem4a  8492  pwfseqlem4  8493  nfseq  11288  rlim2  12245  fsumadd  12487  fsummulc2  12522  fsumrlim  12545  pcmpt  13216  pcmptdvds  13218  prdsdsval2  13661  gsum2d2  15503  gsumcom2  15504  prdsgsum  15507  dprd2d2  15557  gsumdixp  15670  evlslem4  16519  fiuncmp  17421  cnmpt2t  17658  cnmptcom  17663  cnmpt2k  17673  fsumcn  18853  ovoliunlem3  19353  isibl2  19611  nfitg1  19618  nfitg  19619  cbvitg  19620  itgfsum  19671  limciun  19734  dvmptfsum  19812  dvlipcn  19831  lhop2  19852  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem4  19866  dvfsum2  19871  itgparts  19884  itgsubstlem  19885  itgsubst  19886  elplyd  20074  coeeq2  20114  leibpi  20735  rlimcnp  20757  o1cxp  20766  dchrisumlem2  21137  dchrisumlem3  21138  cnlnadjlem5  23527  iundisjf  23982  offval2f  24033  nfesum1  24390  fprodmul  25237  fproddiv  25238  itgabsnc  26173  sdclem1  26337  totbndbnd  26388  ofmpteq  26666  dvdsrabdioph  26760  rfcnpre1  27557  rfcnpre2  27569  mulc1cncfg  27588  expcnfg  27593  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  stoweidlem23  27639  stoweidlem28  27644  stoweidlem36  27652  wallispilem5  27685  stirlinglem15  27704  cdleme26ee  30842  cdleme31se2  30865  cdleme42b  30960  cdlemk11t  31428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator