Theorem nfov 7390

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

Syntax hints:  ⊤wtru 1543  Ⅎwnfc 2884  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  csbov123  7404  ovmpos  7508  ov2gf  7509  ovmpodxf  7510  ovmpodv2  7518  ov3  7523  nfof  7630  offval2f  7639  offval2  7644  ofmpteq  7647  nffrecs  8226  oawordeulem  8482  nnawordex  8566  ttrcltr  9628  pwfseqlem2  10573  pwfseqlem4a  10575  pwfseqlem4  10576  nfseq  13964  rlim2  15449  fsumadd  15693  fsummulc2  15737  fsumrlim  15765  fprodmul  15916  fproddiv  15917  fproddivf  15943  pcmpt  16854  pcmptdvds  16856  prdsdsval2  17438  symgval  19337  gsum2d2  19940  gsumcom2  19941  prdsgsum  19947  dprd2d2  20012  gsumdixp  20289  pwsgprod  20300  evlslem4  22064  gsumply1eq  22284  madugsum  22618  cayleyhamilton1  22867  fiuncmp  23379  cnmpt2t  23648  cnmptcom  23653  cnmpt2k  23663  fsumcn  24847  ovoliunlem3  25481  isibl2  25743  nfitg1  25751  nfitg  25752  cbvitg  25753  itgfsum  25804  limciun  25871  dvmptfsum  25952  dvlipcn  25971  lhop2  25992  dvfsumabs  26000  dvfsumlem1  26003  dvfsumlem4  26006  dvfsum2  26011  itgparts  26024  itgsubstlem  26025  itgsubst  26026  elplyd  26177  coeeq2  26217  leibpi  26919  rlimcnp  26942  o1cxp  26952  dchrisumlem2  27467  dchrisumlem3  27468  nfseqs  28293  numclwlk2lem2f1o  30464  cnlnadjlem5  32157  iundisjf  32674  gsumpart  33139  suppgsumssiun  33148  gsumvsca1  33302  gsumvsca2  33303  rmfsupp2  33314  elrspunidl  33503  deg1prod  33658  nfesum1  34200  nfesum2  34201  esum2d  34253  ptrest  37954  sdclem1  38078  totbndbnd  38124  cdleme26ee  40820  cdleme31se2  40843  cdleme42b  40938  cdlemk11t  41406  dvdsrabdioph  43256  naddwordnexlem4  43847  binomcxplemdvbinom  44798  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  rfcnpre1  45468  rfcnpre2  45480  iunmapss  45662  ssmapsn  45663  infrpgernmpt  45911  caucvgbf  45935  cvgcaule  45937  fsummulc1f  46019  mulc1cncfg  46037  expcnfg  46039  fprodexp  46042  climmulf  46052  climexp  46053  climsuse  46056  climrecf  46057  climaddf  46063  mullimc  46064  idlimc  46074  limcperiod  46076  addlimc  46094  0ellimcdiv  46095  climsubmpt  46106  fnlimabslt  46125  climuz  46190  limsupgt  46224  liminflt  46251  cncfshift  46320  dvmptmulf  46383  dvnmul  46389  dvmptfprodlem  46390  dvmptfprod  46391  stoweidlem23  46469  stoweidlem28  46474  stoweidlem36  46482  wallispilem5  46515  stirlinglem15  46534  fourierdlem20  46573  fourierdlem31  46584  fourierdlem68  46620  fourierdlem80  46632  fourierdlem86  46638  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierdlem115  46667  fourierd  46668  fourierclimd  46669  etransclem2  46682  sge0ltfirp  46846  sge0xaddlem2  46880  sge0xadd  46881  hoimbl2  47111  vonhoire  47118  vonioo  47128  vonicc  47131  vonn0ioo2  47136  vonn0icc2  47138  smflimlem6  47222  ovmpordxf  48827  aacllem  50288