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

Theorem nfov 7008
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 7007 . 2 (⊤ → 𝑥(𝐴𝐹𝐵))
87mptru 1514 1 𝑥(𝐴𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wtru 1508  wnfc 2916  (class class class)co 6978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-iota 6154  df-fv 6198  df-ov 6981
This theorem is referenced by:  csbov123  7019  ovmpos  7116  ov2gf  7117  ovmpodxf  7118  ovmpodv2  7126  ov3  7129  nfof  7234  offval2f  7241  offval2  7246  ofmpteq  7248  oawordeulem  7983  nnawordex  8066  pwfseqlem2  9881  pwfseqlem4a  9883  pwfseqlem4  9884  nfseq  13197  rlim2  14717  fsumadd  14959  fsummulc2  15002  fsumrlim  15029  fprodmul  15177  fproddiv  15178  fproddivf  15204  pcmpt  16087  pcmptdvds  16089  prdsdsval2  16616  gsum2d2  18850  gsumcom2  18851  prdsgsum  18854  dprd2d2  18919  gsumdixp  19085  evlslem4  20004  gsumply1eq  20179  madugsum  20959  cayleyhamilton1  21207  fiuncmp  21719  cnmpt2t  21988  cnmptcom  21993  cnmpt2k  22003  fsumcn  23184  ovoliunlem3  23811  isibl2  24073  nfitg1  24080  nfitg  24081  cbvitg  24082  itgfsum  24133  limciun  24198  dvmptfsum  24278  dvlipcn  24297  lhop2  24318  dvfsumabs  24326  dvfsumlem1  24329  dvfsumlem4  24332  dvfsum2  24337  itgparts  24350  itgsubstlem  24351  itgsubst  24352  elplyd  24498  coeeq2  24538  leibpi  25225  rlimcnp  25248  o1cxp  25257  dchrisumlem2  25771  dchrisumlem3  25772  numclwlk2lem2f1o  27935  numclwlk2lem2f1oOLD  27938  cnlnadjlem5  29632  iundisjf  30108  gsumvsca1  30525  gsumvsca2  30526  rmfsupp2  30545  nfesum1  30943  nfesum2  30944  esum2d  30996  nffrecs  32641  ptrest  34332  sdclem1  34460  totbndbnd  34509  cdleme26ee  36941  cdleme31se2  36964  cdleme42b  37059  cdlemk11t  37527  dvdsrabdioph  38803  binomcxplemdvbinom  40101  binomcxplemdvsum  40103  binomcxplemnotnn0  40104  rfcnpre1  40695  rfcnpre2  40707  iunmapss  40904  ssmapsn  40905  infrpgernmpt  41173  fsummulc1f  41283  mulc1cncfg  41302  expcnfg  41304  fprodexp  41307  climmulf  41317  climexp  41318  climsuse  41321  climrecf  41322  climaddf  41328  mullimc  41329  idlimc  41339  limcperiod  41341  addlimc  41361  0ellimcdiv  41362  climsubmpt  41373  fnlimabslt  41392  climuz  41457  limsupgt  41491  liminflt  41518  cncfshift  41588  dvmptmulf  41653  dvnmul  41659  dvmptfprodlem  41660  dvmptfprod  41661  stoweidlem23  41740  stoweidlem28  41745  stoweidlem36  41753  wallispilem5  41786  stirlinglem15  41805  fourierdlem20  41844  fourierdlem31  41855  fourierdlem68  41891  fourierdlem80  41903  fourierdlem86  41909  fourierdlem103  41926  fourierdlem104  41927  fourierdlem112  41935  fourierdlem115  41938  fourierd  41939  fourierclimd  41940  etransclem2  41953  sge0ltfirp  42114  sge0xaddlem2  42148  sge0xadd  42149  hoimbl2  42379  vonhoire  42386  vonioo  42396  vonicc  42399  vonn0ioo2  42404  vonn0icc2  42406  smflimlem6  42484  ovmpt2rdxf  43752  aacllem  44270
  Copyright terms: Public domain W3C validator