Theorem nfov 7388

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

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

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 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  csbov123  7402  ovmpos  7506  ov2gf  7507  ovmpodxf  7508  ovmpodv2  7516  ov3  7521  nfof  7628  offval2f  7637  offval2  7642  ofmpteq  7645  nffrecs  8224  oawordeulem  8480  nnawordex  8564  ttrcltr  9626  pwfseqlem2  10571  pwfseqlem4a  10573  pwfseqlem4  10574  nfseq  13935  rlim2  15420  fsumadd  15664  fsummulc2  15708  fsumrlim  15735  fprodmul  15884  fproddiv  15885  fproddivf  15911  pcmpt  16821  pcmptdvds  16823  prdsdsval2  17405  symgval  19304  gsum2d2  19907  gsumcom2  19908  prdsgsum  19914  dprd2d2  19979  gsumdixp  20256  pwsgprod  20267  evlslem4  22032  gsumply1eq  22252  madugsum  22586  cayleyhamilton1  22835  fiuncmp  23347  cnmpt2t  23616  cnmptcom  23621  cnmpt2k  23631  fsumcn  24815  ovoliunlem3  25449  isibl2  25711  nfitg1  25719  nfitg  25720  cbvitg  25721  itgfsum  25772  limciun  25839  dvmptfsum  25920  dvlipcn  25940  lhop2  25961  dvfsumabs  25970  dvfsumlem1  25973  dvfsumlem4  25977  dvfsum2  25982  itgparts  25995  itgsubstlem  25996  itgsubst  25997  elplyd  26148  coeeq2  26188  leibpi  26892  rlimcnp  26915  o1cxp  26925  dchrisumlem2  27441  dchrisumlem3  27442  nfseqs  28267  numclwlk2lem2f1o  30438  cnlnadjlem5  32131  iundisjf  32648  gsumpart  33129  suppgsumssiun  33138  gsumvsca1  33292  gsumvsca2  33293  rmfsupp2  33304  elrspunidl  33493  deg1prod  33648  nfesum1  34190  nfesum2  34191  esum2d  34243  ptrest  37931  sdclem1  38055  totbndbnd  38101  cdleme26ee  40797  cdleme31se2  40820  cdleme42b  40915  cdlemk11t  41383  dvdsrabdioph  43241  naddwordnexlem4  43832  binomcxplemdvbinom  44783  binomcxplemdvsum  44785  binomcxplemnotnn0  44786  rfcnpre1  45453  rfcnpre2  45465  iunmapss  45647  ssmapsn  45648  infrpgernmpt  45897  caucvgbf  45921  cvgcaule  45923  fsummulc1f  46005  mulc1cncfg  46023  expcnfg  46025  fprodexp  46028  climmulf  46038  climexp  46039  climsuse  46042  climrecf  46043  climaddf  46049  mullimc  46050  idlimc  46060  limcperiod  46062  addlimc  46080  0ellimcdiv  46081  climsubmpt  46092  fnlimabslt  46111  climuz  46176  limsupgt  46210  liminflt  46237  cncfshift  46306  dvmptmulf  46369  dvnmul  46375  dvmptfprodlem  46376  dvmptfprod  46377  stoweidlem23  46455  stoweidlem28  46460  stoweidlem36  46468  wallispilem5  46501  stirlinglem15  46520  fourierdlem20  46559  fourierdlem31  46570  fourierdlem68  46606  fourierdlem80  46618  fourierdlem86  46624  fourierdlem103  46641  fourierdlem104  46642  fourierdlem112  46650  fourierdlem115  46653  fourierd  46654  fourierclimd  46655  etransclem2  46668  sge0ltfirp  46832  sge0xaddlem2  46866  sge0xadd  46867  hoimbl2  47097  vonhoire  47104  vonioo  47114  vonicc  47117  vonn0ioo2  47122  vonn0icc2  47124  smflimlem6  47208  ovmpordxf  48773  aacllem  50234