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

Theorem nfov 6716
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 6715 . 2 (⊤ → 𝑥(𝐴𝐹𝐵))
87trud 1533 1 𝑥(𝐴𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1524  wnfc 2780  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  csbov123  6727  ovmpt2s  6826  ov2gf  6827  ovmpt2dxf  6828  ovmpt2dv2  6836  ov3  6839  offval2f  6951  offval2  6956  ofmpteq  6958  oawordeulem  7679  nnawordex  7762  pwfseqlem2  9519  pwfseqlem4a  9521  pwfseqlem4  9522  nfseq  12851  rlim2  14271  fsumadd  14514  fsummulc2  14560  fsumrlim  14587  fprodmul  14734  fproddiv  14735  fproddivf  14762  pcmpt  15643  pcmptdvds  15645  prdsdsval2  16191  gsum2d2  18419  gsumcom2  18420  prdsgsum  18423  dprd2d2  18489  gsumdixp  18655  evlslem4  19556  gsumply1eq  19723  madugsum  20497  cayleyhamilton1  20745  fiuncmp  21255  cnmpt2t  21524  cnmptcom  21529  cnmpt2k  21539  fsumcn  22720  ovoliunlem3  23318  isibl2  23578  nfitg1  23585  nfitg  23586  cbvitg  23587  itgfsum  23638  limciun  23703  dvmptfsum  23783  dvlipcn  23802  lhop2  23823  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem4  23837  dvfsum2  23842  itgparts  23855  itgsubstlem  23856  itgsubst  23857  elplyd  24003  coeeq2  24043  leibpi  24714  rlimcnp  24737  o1cxp  24746  dchrisumlem2  25224  dchrisumlem3  25225  numclwlk1lem2  27350  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  cnlnadjlem5  29058  iundisjf  29528  gsumvsca1  29910  gsumvsca2  29911  nfesum1  30230  nfesum2  30231  esum2d  30283  nffrecs  31903  ptrest  33538  sdclem1  33669  totbndbnd  33718  cdleme26ee  35965  cdleme31se2  35988  cdleme42b  36083  cdlemk11t  36551  dvdsrabdioph  37691  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  rfcnpre1  39492  rfcnpre2  39504  iunmapss  39721  ssmapsn  39722  infrpgernmpt  40008  fsummulc1f  40120  mulc1cncfg  40139  expcnfg  40141  fprodexp  40144  climmulf  40154  climexp  40155  climsuse  40158  climrecf  40159  climaddf  40165  mullimc  40166  idlimc  40176  limcperiod  40178  addlimc  40198  0ellimcdiv  40199  climsubmpt  40210  fnlimabslt  40229  climuz  40294  limsupgt  40328  liminflt  40355  cncfshift  40405  dvmptmulf  40470  dvnmul  40476  dvmptfprodlem  40477  dvmptfprod  40478  stoweidlem23  40558  stoweidlem28  40563  stoweidlem36  40571  wallispilem5  40604  stirlinglem15  40623  fourierdlem20  40662  fourierdlem31  40673  fourierdlem68  40709  fourierdlem80  40721  fourierdlem86  40727  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem115  40756  fourierd  40757  fourierclimd  40758  etransclem2  40771  sge0ltfirp  40935  sge0xaddlem2  40969  sge0xadd  40970  hoimbl2  41200  vonhoire  41207  vonioo  41217  vonicc  41220  vonn0ioo2  41225  vonn0icc2  41227  smflimlem6  41305  ovmpt2rdxf  42442  aacllem  42875
  Copyright terms: Public domain W3C validator