Theorem nfov 7384

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

Syntax hints:  ⊤wtru 1542  Ⅎwnfc 2880  (class class class)co 7354

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6444  df-fv 6496  df-ov 7357

This theorem is referenced by:  csbov123  7398  ovmpos  7502  ov2gf  7503  ovmpodxf  7504  ovmpodv2  7512  ov3  7517  nfof  7624  offval2f  7633  offval2  7638  ofmpteq  7641  nffrecs  8221  oawordeulem  8477  nnawordex  8560  ttrcltr  9615  pwfseqlem2  10559  pwfseqlem4a  10561  pwfseqlem4  10562  nfseq  13922  rlim2  15407  fsumadd  15651  fsummulc2  15695  fsumrlim  15722  fprodmul  15871  fproddiv  15872  fproddivf  15898  pcmpt  16808  pcmptdvds  16810  prdsdsval2  17392  symgval  19287  gsum2d2  19890  gsumcom2  19891  prdsgsum  19897  dprd2d2  19962  gsumdixp  20241  evlslem4  22014  gsumply1eq  22227  madugsum  22561  cayleyhamilton1  22810  fiuncmp  23322  cnmpt2t  23591  cnmptcom  23596  cnmpt2k  23606  fsumcn  24791  ovoliunlem3  25435  isibl2  25697  nfitg1  25705  nfitg  25706  cbvitg  25707  itgfsum  25758  limciun  25825  dvmptfsum  25909  dvlipcn  25929  lhop2  25950  dvfsumabs  25959  dvfsumlem1  25962  dvfsumlem4  25966  dvfsum2  25971  itgparts  25984  itgsubstlem  25985  itgsubst  25986  elplyd  26137  coeeq2  26177  leibpi  26882  rlimcnp  26905  o1cxp  26915  dchrisumlem2  27431  dchrisumlem3  27432  nfseqs  28220  numclwlk2lem2f1o  30363  cnlnadjlem5  32055  iundisjf  32573  gsumpart  33046  gsumvsca1  33204  gsumvsca2  33205  rmfsupp2  33214  elrspunidl  33402  nfesum1  34076  nfesum2  34077  esum2d  34129  ptrest  37682  sdclem1  37806  totbndbnd  37852  cdleme26ee  40482  cdleme31se2  40505  cdleme42b  40600  cdlemk11t  41068  pwsgprod  42665  dvdsrabdioph  42930  naddwordnexlem4  43521  binomcxplemdvbinom  44473  binomcxplemdvsum  44475  binomcxplemnotnn0  44476  rfcnpre1  45143  rfcnpre2  45155  iunmapss  45339  ssmapsn  45340  infrpgernmpt  45590  caucvgbf  45614  cvgcaule  45616  fsummulc1f  45698  mulc1cncfg  45716  expcnfg  45718  fprodexp  45721  climmulf  45731  climexp  45732  climsuse  45735  climrecf  45736  climaddf  45742  mullimc  45743  idlimc  45753  limcperiod  45755  addlimc  45773  0ellimcdiv  45774  climsubmpt  45785  fnlimabslt  45804  climuz  45869  limsupgt  45903  liminflt  45930  cncfshift  45999  dvmptmulf  46062  dvnmul  46068  dvmptfprodlem  46069  dvmptfprod  46070  stoweidlem23  46148  stoweidlem28  46153  stoweidlem36  46161  wallispilem5  46194  stirlinglem15  46213  fourierdlem20  46252  fourierdlem31  46263  fourierdlem68  46299  fourierdlem80  46311  fourierdlem86  46317  fourierdlem103  46334  fourierdlem104  46335  fourierdlem112  46343  fourierdlem115  46346  fourierd  46347  fourierclimd  46348  etransclem2  46361  sge0ltfirp  46525  sge0xaddlem2  46559  sge0xadd  46560  hoimbl2  46790  vonhoire  46797  vonioo  46807  vonicc  46810  vonn0ioo2  46815  vonn0icc2  46817  smflimlem6  46901  ovmpordxf  48466  aacllem  49929