Theorem nfov 7444

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

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

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417

This theorem is used by:  csbov123  7458  ovmpos  7562  ov2gf  7563  ovmpodxf  7564  ovmpodv2  7572  ov3  7577  nfof  7685  offval2f  7694  offval2  7699  ofmpteq  7702  nffrecs  8283  oawordeulem  8544  nnawordex  8628  ttrcltr  9698  pwfseqlem2  10671  pwfseqlem4a  10673  pwfseqlem4  10674  nfseq  14078  rlim2  15586  fsumadd  15829  fsummulc2  15873  fsumrlim  15901  fprodmul  16050  fproddiv  16051  fproddivf  16077  pcmpt  16987  pcmptdvds  16989  prdsdsval2  17572  symgval  19501  gsum2d2  20104  gsumcom2  20105  prdsgsum  20111  dprd2d2  20176  gsumdixp  20462  pwsgprod  20473  evlslem4  22295  gsumply1eq  22537  madugsum  22868  cayleyhamilton1  23120  fiuncmp  23632  cnmpt2t  23902  cnmptcom  23907  cnmpt2k  23917  fsumcn  25101  ovoliunlem3  25735  isibl2  25997  nfitg1  26004  nfitg  26005  cbvitg  26006  itgfsum  26057  limciun  26124  dvmptfsum  26205  dvlipcn  26224  lhop2  26245  dvfsumabs  26253  dvfsumlem1  26256  dvfsumlem4  26259  dvfsum2  26264  itgparts  26277  itgsubstlem  26278  itgsubst  26279  elplyd  26430  coeeq2  26471  leibpi  27182  rlimcnp  27205  o1cxp  27214  dchrisumlem2  27729  dchrisumlem3  27730  nfseqs  28555  numclwlk2lem2f1o  30862  cnlnadjlem5  32555  iundisjf  33065  gsumpart  33506  suppgsumssiun  33515  gsumvsca1  33669  gsumvsca2  33670  rmfsupp2  33680  elrspunidl  33859  deg1prod  33996  nfesum1  34553  nfesum2  34554  esum2d  34606  ptrest  38371  sdclem1  38496  totbndbnd  38542  cdleme26ee  41236  cdleme31se2  41259  cdleme42b  41354  cdlemk11t  41822  dvdsrabdioph  43654  naddwordnexlem4  44245  binomcxplemdvbinom  45180  binomcxplemdvsum  45182  binomcxplemnotnn0  45183  rfcnpre1  45856  rfcnpre2  45868  iunmapss  46048  ssmapsn  46049  infrpgernmpt  46296  caucvgbf  46320  cvgcaule  46322  fsummulc1f  46404  mulc1cncfg  46422  expcnfg  46424  fprodexp  46427  climmulf  46437  climexp  46438  climsuse  46441  climrecf  46442  climaddf  46448  mullimc  46449  idlimc  46459  limcperiod  46461  addlimc  46479  0ellimcdiv  46480  climsubmpt  46491  fnlimabslt  46510  climuz  46575  limsupgt  46609  liminflt  46636  cncfshift  46705  dvmptmulf  46768  dvnmul  46774  dvmptfprodlem  46775  dvmptfprod  46776  stoweidlem23  46854  stoweidlem28  46859  stoweidlem36  46867  wallispilem5  46900  stirlinglem15  46919  fourierdlem20  46958  fourierdlem31  46969  fourierdlem68  47005  fourierdlem80  47017  fourierdlem86  47023  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  fourierdlem115  47052  fourierd  47053  fourierclimd  47054  etransclem2  47067  sge0ltfirp  47231  sge0xaddlem2  47265  sge0xadd  47266  hoimbl2  47496  vonhoire  47503  vonioo  47513  vonicc  47516  vonn0ioo2  47521  vonn0icc2  47523  smflimlem6  47607  ovmpordxf  49272  aacllem  50775