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

Theorem nfov 6553
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 6552 . 2 (⊤ → 𝑥(𝐴𝐹𝐵))
87trud 1483 1 𝑥(𝐴𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1475  wnfc 2737  (class class class)co 6527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  csbov123  6563  ovmpt2s  6660  ov2gf  6661  ovmpt2dxf  6662  ovmpt2dv2  6670  ov3  6673  offval2f  6784  offval2  6789  ofmpteq  6791  oawordeulem  7498  nnawordex  7581  pwfseqlem2  9337  pwfseqlem4a  9339  pwfseqlem4  9340  nfseq  12628  rlim2  14021  fsumadd  14263  fsummulc2  14304  fsumrlim  14330  fprodmul  14475  fproddiv  14476  fproddivf  14503  pcmpt  15380  pcmptdvds  15382  prdsdsval2  15913  gsum2d2  18142  gsumcom2  18143  prdsgsum  18146  dprd2d2  18212  gsumdixp  18378  evlslem4  19275  gsumply1eq  19442  madugsum  20210  cayleyhamilton1  20458  fiuncmp  20959  cnmpt2t  21228  cnmptcom  21233  cnmpt2k  21243  fsumcn  22412  ovoliunlem3  22996  isibl2  23256  nfitg1  23263  nfitg  23264  cbvitg  23265  itgfsum  23316  limciun  23381  dvmptfsum  23459  dvlipcn  23478  lhop2  23499  dvfsumabs  23507  dvfsumlem1  23510  dvfsumlem4  23513  dvfsum2  23518  itgparts  23531  itgsubstlem  23532  itgsubst  23533  elplyd  23679  coeeq2  23719  leibpi  24386  rlimcnp  24409  o1cxp  24418  dchrisumlem2  24896  dchrisumlem3  24897  cnlnadjlem5  28120  iundisjf  28590  gsumvsca1  28919  gsumvsca2  28920  nfesum1  29235  nfesum2  29236  esum2d  29288  ptrest  32381  sdclem1  32512  totbndbnd  32561  cdleme26ee  34469  cdleme31se2  34492  cdleme42b  34587  cdlemk11t  35055  dvdsrabdioph  36195  binomcxplemdvbinom  37377  binomcxplemdvsum  37379  binomcxplemnotnn0  37380  rfcnpre1  38004  rfcnpre2  38016  iunmapss  38205  ssmapsn  38206  fsummulc1f  38439  mulc1cncfg  38460  expcnfg  38462  fprodexp  38465  climmulf  38475  climexp  38476  climsuse  38479  climrecf  38480  climaddf  38486  mullimc  38487  idlimc  38497  limcperiod  38499  addlimc  38519  0ellimcdiv  38520  climsubmpt  38531  fnlimabslt  38550  cncfshift  38563  dvmptmulf  38631  dvnmul  38637  dvmptfprodlem  38638  dvmptfprod  38639  stoweidlem23  38720  stoweidlem28  38725  stoweidlem36  38733  wallispilem5  38766  stirlinglem15  38785  fourierdlem20  38824  fourierdlem31  38835  fourierdlem68  38871  fourierdlem80  38883  fourierdlem86  38889  fourierdlem103  38906  fourierdlem104  38907  fourierdlem112  38915  fourierdlem115  38918  fourierd  38919  fourierclimd  38920  etransclem2  38933  sge0ltfirp  39097  sge0xaddlem2  39131  sge0xadd  39132  hoimbl2  39359  vonhoire  39367  vonioo  39377  vonicc  39380  vonn0ioo2  39385  vonn0icc2  39387  smflimlem6  39466  ovmpt2rdxf  41912  aacllem  42319
  Copyright terms: Public domain W3C validator