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

Theorem nfov 6641
Description: Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
Hypotheses
Ref Expression
nfov.1 𝑥𝐴
nfov.2 𝑥𝐹
nfov.3 𝑥𝐵
Assertion
Ref Expression
nfov 𝑥(𝐴𝐹𝐵)

Proof of Theorem nfov
StepHypRef Expression
1 nfov.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfov.2 . . . 4 𝑥𝐹
43a1i 11 . . 3 (⊤ → 𝑥𝐹)
5 nfov.3 . . . 4 𝑥𝐵
65a1i 11 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfovd 6640 . 2 (⊤ → 𝑥(𝐴𝐹𝐵))
87trud 1490 1 𝑥(𝐴𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1481  wnfc 2748  (class class class)co 6615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618
This theorem is referenced by:  csbov123  6652  ovmpt2s  6749  ov2gf  6750  ovmpt2dxf  6751  ovmpt2dv2  6759  ov3  6762  offval2f  6874  offval2  6879  ofmpteq  6881  oawordeulem  7594  nnawordex  7677  pwfseqlem2  9441  pwfseqlem4a  9443  pwfseqlem4  9444  nfseq  12767  rlim2  14177  fsumadd  14419  fsummulc2  14463  fsumrlim  14489  fprodmul  14634  fproddiv  14635  fproddivf  14662  pcmpt  15539  pcmptdvds  15541  prdsdsval2  16084  gsum2d2  18313  gsumcom2  18314  prdsgsum  18317  dprd2d2  18383  gsumdixp  18549  evlslem4  19448  gsumply1eq  19615  madugsum  20389  cayleyhamilton1  20637  fiuncmp  21147  cnmpt2t  21416  cnmptcom  21421  cnmpt2k  21431  fsumcn  22613  ovoliunlem3  23212  isibl2  23473  nfitg1  23480  nfitg  23481  cbvitg  23482  itgfsum  23533  limciun  23598  dvmptfsum  23676  dvlipcn  23695  lhop2  23716  dvfsumabs  23724  dvfsumlem1  23727  dvfsumlem4  23730  dvfsum2  23735  itgparts  23748  itgsubstlem  23749  itgsubst  23750  elplyd  23896  coeeq2  23936  leibpi  24603  rlimcnp  24626  o1cxp  24635  dchrisumlem2  25113  dchrisumlem3  25114  cnlnadjlem5  28818  iundisjf  29288  gsumvsca1  29609  gsumvsca2  29610  nfesum1  29925  nfesum2  29926  esum2d  29978  ptrest  33079  sdclem1  33210  totbndbnd  33259  cdleme26ee  35167  cdleme31se2  35190  cdleme42b  35285  cdlemk11t  35753  dvdsrabdioph  36893  binomcxplemdvbinom  38073  binomcxplemdvsum  38075  binomcxplemnotnn0  38076  rfcnpre1  38700  rfcnpre2  38712  iunmapss  38916  ssmapsn  38917  fsummulc1f  39238  mulc1cncfg  39257  expcnfg  39259  fprodexp  39262  climmulf  39272  climexp  39273  climsuse  39276  climrecf  39277  climaddf  39283  mullimc  39284  idlimc  39294  limcperiod  39296  addlimc  39316  0ellimcdiv  39317  climsubmpt  39328  fnlimabslt  39347  cncfshift  39422  dvmptmulf  39489  dvnmul  39495  dvmptfprodlem  39496  dvmptfprod  39497  stoweidlem23  39577  stoweidlem28  39582  stoweidlem36  39590  wallispilem5  39623  stirlinglem15  39642  fourierdlem20  39681  fourierdlem31  39692  fourierdlem68  39728  fourierdlem80  39740  fourierdlem86  39746  fourierdlem103  39763  fourierdlem104  39764  fourierdlem112  39772  fourierdlem115  39775  fourierd  39776  fourierclimd  39777  etransclem2  39790  sge0ltfirp  39954  sge0xaddlem2  39988  sge0xadd  39989  hoimbl2  40216  vonhoire  40223  vonioo  40233  vonicc  40236  vonn0ioo2  40241  vonn0icc2  40243  smflimlem6  40321  ovmpt2rdxf  41435  aacllem  41880
  Copyright terms: Public domain W3C validator