Theorem nfov 7446

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 7445	. 2 ⊢ (⊤ → Ⅎ𝑥(𝐴𝐹𝐵))
8	7	mptru 1577	1 ⊢ Ⅎ𝑥(𝐴𝐹𝐵)

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnfc 2912  (class class class)co 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419

This theorem is used by:  csbov123  7460  ovmpos  7564  ov2gf  7565  ovmpodxf  7566  ovmpodv2  7574  ov3  7579  nfof  7686  offval2f  7695  offval2  7700  ofmpteq  7703  nffrecs  8282  oawordeulem  8541  nnawordex  8625  ttrcltr  9688  pwfseqlem2  10655  pwfseqlem4a  10657  pwfseqlem4  10658  nfseq  14060  rlim2  15566  fsumadd  15809  fsummulc2  15853  fsumrlim  15881  fprodmul  16032  fproddiv  16033  fproddivf  16059  pcmpt  16969  pcmptdvds  16971  prdsdsval2  17554  symgval  19464  gsum2d2  20067  gsumcom2  20068  prdsgsum  20074  dprd2d2  20139  gsumdixp  20425  pwsgprod  20436  evlslem4  22256  gsumply1eq  22498  madugsum  22829  cayleyhamilton1  23078  fiuncmp  23590  cnmpt2t  23859  cnmptcom  23864  cnmpt2k  23874  fsumcn  25058  ovoliunlem3  25692  isibl2  25954  nfitg1  25962  nfitg  25963  cbvitg  25964  itgfsum  26015  limciun  26082  dvmptfsum  26163  dvlipcn  26182  lhop2  26203  dvfsumabs  26211  dvfsumlem1  26214  dvfsumlem4  26217  dvfsum2  26222  itgparts  26235  itgsubstlem  26236  itgsubst  26237  elplyd  26388  coeeq2  26428  leibpi  27136  rlimcnp  27159  o1cxp  27168  dchrisumlem2  27683  dchrisumlem3  27684  nfseqs  28509  numclwlk2lem2f1o  30759  cnlnadjlem5  32452  iundisjf  32963  gsumpart  33406  suppgsumssiun  33415  gsumvsca1  33569  gsumvsca2  33570  rmfsupp2  33580  elrspunidl  33759  deg1prod  33896  nfesum1  34453  nfesum2  34454  esum2d  34506  ptrest  38303  sdclem1  38427  totbndbnd  38473  cdleme26ee  41167  cdleme31se2  41190  cdleme42b  41285  cdlemk11t  41753  dvdsrabdioph  43570  naddwordnexlem4  44161  binomcxplemdvbinom  45096  binomcxplemdvsum  45098  binomcxplemnotnn0  45099  rfcnpre1  45772  rfcnpre2  45784  iunmapss  45964  ssmapsn  45965  infrpgernmpt  46212  caucvgbf  46236  cvgcaule  46238  fsummulc1f  46320  mulc1cncfg  46338  expcnfg  46340  fprodexp  46343  climmulf  46353  climexp  46354  climsuse  46357  climrecf  46358  climaddf  46364  mullimc  46365  idlimc  46375  limcperiod  46377  addlimc  46395  0ellimcdiv  46396  climsubmpt  46407  fnlimabslt  46426  climuz  46491  limsupgt  46525  liminflt  46552  cncfshift  46621  dvmptmulf  46684  dvnmul  46690  dvmptfprodlem  46691  dvmptfprod  46692  stoweidlem23  46770  stoweidlem28  46775  stoweidlem36  46783  wallispilem5  46816  stirlinglem15  46835  fourierdlem20  46874  fourierdlem31  46885  fourierdlem68  46921  fourierdlem80  46933  fourierdlem86  46939  fourierdlem103  46956  fourierdlem104  46957  fourierdlem112  46965  fourierdlem115  46968  fourierd  46969  fourierclimd  46970  etransclem2  46983  sge0ltfirp  47147  sge0xaddlem2  47181  sge0xadd  47182  hoimbl2  47412  vonhoire  47419  vonioo  47429  vonicc  47432  vonn0ioo2  47437  vonn0icc2  47439  smflimlem6  47523  ovmpordxf  49152  aacllem  50654