Theorem nfov 7376

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

Step	Hyp	Ref	Expression
1		nfov.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfov.2	. . . 4 ⊢ Ⅎ𝑥𝐹
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐹)
5		nfov.3	. . . 4 ⊢ Ⅎ𝑥𝐵
6	5	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
7	2, 4, 6	nfovd 7375	. 2 ⊢ (⊤ → Ⅎ𝑥(𝐴𝐹𝐵))
8	7	mptru 1548	1 ⊢ Ⅎ𝑥(𝐴𝐹𝐵)

Syntax hints:  ⊤wtru 1542  Ⅎwnfc 2879  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  csbov123  7390  ovmpos  7494  ov2gf  7495  ovmpodxf  7496  ovmpodv2  7504  ov3  7509  nfof  7616  offval2f  7625  offval2  7630  ofmpteq  7633  nffrecs  8213  oawordeulem  8469  nnawordex  8552  ttrcltr  9606  pwfseqlem2  10550  pwfseqlem4a  10552  pwfseqlem4  10553  nfseq  13918  rlim2  15403  fsumadd  15647  fsummulc2  15691  fsumrlim  15718  fprodmul  15867  fproddiv  15868  fproddivf  15894  pcmpt  16804  pcmptdvds  16806  prdsdsval2  17388  symgval  19284  gsum2d2  19887  gsumcom2  19888  prdsgsum  19894  dprd2d2  19959  gsumdixp  20238  evlslem4  22012  gsumply1eq  22225  madugsum  22559  cayleyhamilton1  22808  fiuncmp  23320  cnmpt2t  23589  cnmptcom  23594  cnmpt2k  23604  fsumcn  24789  ovoliunlem3  25433  isibl2  25695  nfitg1  25703  nfitg  25704  cbvitg  25705  itgfsum  25756  limciun  25823  dvmptfsum  25907  dvlipcn  25927  lhop2  25948  dvfsumabs  25957  dvfsumlem1  25960  dvfsumlem4  25964  dvfsum2  25969  itgparts  25982  itgsubstlem  25983  itgsubst  25984  elplyd  26135  coeeq2  26175  leibpi  26880  rlimcnp  26903  o1cxp  26913  dchrisumlem2  27429  dchrisumlem3  27430  nfseqs  28218  numclwlk2lem2f1o  30357  cnlnadjlem5  32049  iundisjf  32567  gsumpart  33035  gsumvsca1  33193  gsumvsca2  33194  rmfsupp2  33203  elrspunidl  33391  nfesum1  34051  nfesum2  34052  esum2d  34104  ptrest  37665  sdclem1  37789  totbndbnd  37835  cdleme26ee  40405  cdleme31se2  40428  cdleme42b  40523  cdlemk11t  40991  pwsgprod  42583  dvdsrabdioph  42849  naddwordnexlem4  43440  binomcxplemdvbinom  44392  binomcxplemdvsum  44394  binomcxplemnotnn0  44395  rfcnpre1  45062  rfcnpre2  45074  iunmapss  45258  ssmapsn  45259  infrpgernmpt  45509  caucvgbf  45533  cvgcaule  45535  fsummulc1f  45617  mulc1cncfg  45635  expcnfg  45637  fprodexp  45640  climmulf  45650  climexp  45651  climsuse  45654  climrecf  45655  climaddf  45661  mullimc  45662  idlimc  45672  limcperiod  45674  addlimc  45692  0ellimcdiv  45693  climsubmpt  45704  fnlimabslt  45723  climuz  45788  limsupgt  45822  liminflt  45849  cncfshift  45918  dvmptmulf  45981  dvnmul  45987  dvmptfprodlem  45988  dvmptfprod  45989  stoweidlem23  46067  stoweidlem28  46072  stoweidlem36  46080  wallispilem5  46113  stirlinglem15  46132  fourierdlem20  46171  fourierdlem31  46182  fourierdlem68  46218  fourierdlem80  46230  fourierdlem86  46236  fourierdlem103  46253  fourierdlem104  46254  fourierdlem112  46262  fourierdlem115  46265  fourierd  46266  fourierclimd  46267  etransclem2  46280  sge0ltfirp  46444  sge0xaddlem2  46478  sge0xadd  46479  hoimbl2  46709  vonhoire  46716  vonioo  46726  vonicc  46729  vonn0ioo2  46734  vonn0icc2  46736  smflimlem6  46820  ovmpordxf  48376  aacllem  49839