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

Theorem nfov 7179
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 7178 . 2 (⊤ → 𝑥(𝐴𝐹𝐵))
87mptru 1545 1 𝑥(𝐴𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1539  wnfc 2962  (class class class)co 7149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7152
This theorem is referenced by:  csbov123  7191  ovmpos  7291  ov2gf  7292  ovmpodxf  7293  ovmpodv2  7301  ov3  7305  nfof  7408  offval2f  7415  offval2  7420  ofmpteq  7422  oawordeulem  8176  nnawordex  8259  pwfseqlem2  10079  pwfseqlem4a  10081  pwfseqlem4  10082  nfseq  13383  rlim2  14853  fsumadd  15096  fsummulc2  15139  fsumrlim  15166  fprodmul  15314  fproddiv  15315  fproddivf  15341  pcmpt  16226  pcmptdvds  16228  prdsdsval2  16757  symgval  18497  gsum2d2  19094  gsumcom2  19095  prdsgsum  19101  dprd2d2  19166  gsumdixp  19362  evlslem4  20754  gsumply1eq  20941  madugsum  21255  cayleyhamilton1  21503  fiuncmp  22015  cnmpt2t  22284  cnmptcom  22289  cnmpt2k  22299  fsumcn  23481  ovoliunlem3  24114  isibl2  24376  nfitg1  24383  nfitg  24384  cbvitg  24385  itgfsum  24436  limciun  24503  dvmptfsum  24584  dvlipcn  24603  lhop2  24624  dvfsumabs  24632  dvfsumlem1  24635  dvfsumlem4  24638  dvfsum2  24643  itgparts  24656  itgsubstlem  24657  itgsubst  24658  elplyd  24805  coeeq2  24845  leibpi  25534  rlimcnp  25557  o1cxp  25566  dchrisumlem2  26080  dchrisumlem3  26081  numclwlk2lem2f1o  28170  cnlnadjlem5  29860  iundisjf  30353  gsumvsca1  30889  gsumvsca2  30890  rmfsupp2  30902  nfesum1  31359  nfesum2  31360  esum2d  31412  nffrecs  33180  ptrest  35004  sdclem1  35129  totbndbnd  35175  cdleme26ee  37604  cdleme31se2  37627  cdleme42b  37722  cdlemk11t  38190  dvdsrabdioph  39671  binomcxplemdvbinom  40981  binomcxplemdvsum  40983  binomcxplemnotnn0  40984  rfcnpre1  41572  rfcnpre2  41584  iunmapss  41773  ssmapsn  41774  infrpgernmpt  42034  fsummulc1f  42142  mulc1cncfg  42161  expcnfg  42163  fprodexp  42166  climmulf  42176  climexp  42177  climsuse  42180  climrecf  42181  climaddf  42187  mullimc  42188  idlimc  42198  limcperiod  42200  addlimc  42220  0ellimcdiv  42221  climsubmpt  42232  fnlimabslt  42251  climuz  42316  limsupgt  42350  liminflt  42377  cncfshift  42446  dvmptmulf  42509  dvnmul  42515  dvmptfprodlem  42516  dvmptfprod  42517  stoweidlem23  42595  stoweidlem28  42600  stoweidlem36  42608  wallispilem5  42641  stirlinglem15  42660  fourierdlem20  42699  fourierdlem31  42710  fourierdlem68  42746  fourierdlem80  42758  fourierdlem86  42764  fourierdlem103  42781  fourierdlem104  42782  fourierdlem112  42790  fourierdlem115  42793  fourierd  42794  fourierclimd  42795  etransclem2  42808  sge0ltfirp  42969  sge0xaddlem2  43003  sge0xadd  43004  hoimbl2  43234  vonhoire  43241  vonioo  43251  vonicc  43254  vonn0ioo2  43259  vonn0icc2  43261  smflimlem6  43339  ovmpordxf  44670  aacllem  45259
  Copyright terms: Public domain W3C validator