Theorem nfov 7393

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

Syntax hints:  ⊤wtru 1548  Ⅎwnfc 2887  (class class class)co 7363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  csbov123  7407  ovmpos  7511  ov2gf  7512  ovmpodxf  7513  ovmpodv2  7521  ov3  7526  nfof  7633  offval2f  7642  offval2  7647  ofmpteq  7650  nffrecs  8230  oawordeulem  8486  nnawordex  8570  ttrcltr  9635  pwfseqlem2  10580  pwfseqlem4a  10582  pwfseqlem4  10583  nfseq  13971  rlim2  15456  fsumadd  15700  fsummulc2  15744  fsumrlim  15772  fprodmul  15923  fproddiv  15924  fproddivf  15950  pcmpt  16861  pcmptdvds  16863  prdsdsval2  17445  symgval  19344  gsum2d2  19947  gsumcom2  19948  prdsgsum  19954  dprd2d2  20019  gsumdixp  20296  pwsgprod  20307  evlslem4  22059  gsumply1eq  22302  madugsum  22633  cayleyhamilton1  22882  fiuncmp  23394  cnmpt2t  23663  cnmptcom  23668  cnmpt2k  23678  fsumcn  24862  ovoliunlem3  25496  isibl2  25758  nfitg1  25766  nfitg  25767  cbvitg  25768  itgfsum  25819  limciun  25886  dvmptfsum  25967  dvlipcn  25986  lhop2  26007  dvfsumabs  26015  dvfsumlem1  26018  dvfsumlem4  26021  dvfsum2  26026  itgparts  26039  itgsubstlem  26040  itgsubst  26041  elplyd  26192  coeeq2  26232  leibpi  26931  rlimcnp  26954  o1cxp  26963  dchrisumlem2  27478  dchrisumlem3  27479  nfseqs  28304  numclwlk2lem2f1o  30474  cnlnadjlem5  32167  iundisjf  32685  gsumpart  33151  suppgsumssiun  33160  gsumvsca1  33314  gsumvsca2  33315  rmfsupp2  33326  elrspunidl  33518  deg1prod  33673  nfesum1  34231  nfesum2  34232  esum2d  34284  ptrest  37993  sdclem1  38117  totbndbnd  38163  cdleme26ee  40859  cdleme31se2  40882  cdleme42b  40977  cdlemk11t  41445  dvdsrabdioph  43262  naddwordnexlem4  43853  binomcxplemdvbinom  44804  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  rfcnpre1  45474  rfcnpre2  45486  iunmapss  45667  ssmapsn  45668  infrpgernmpt  45915  caucvgbf  45939  cvgcaule  45941  fsummulc1f  46023  mulc1cncfg  46041  expcnfg  46043  fprodexp  46046  climmulf  46056  climexp  46057  climsuse  46060  climrecf  46061  climaddf  46067  mullimc  46068  idlimc  46078  limcperiod  46080  addlimc  46098  0ellimcdiv  46099  climsubmpt  46110  fnlimabslt  46129  climuz  46194  limsupgt  46228  liminflt  46255  cncfshift  46324  dvmptmulf  46387  dvnmul  46393  dvmptfprodlem  46394  dvmptfprod  46395  stoweidlem23  46473  stoweidlem28  46478  stoweidlem36  46486  wallispilem5  46519  stirlinglem15  46538  fourierdlem20  46577  fourierdlem31  46588  fourierdlem68  46624  fourierdlem80  46636  fourierdlem86  46642  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem115  46671  fourierd  46672  fourierclimd  46673  etransclem2  46686  sge0ltfirp  46850  sge0xaddlem2  46884  sge0xadd  46885  hoimbl2  47115  vonhoire  47122  vonioo  47132  vonicc  47135  vonn0ioo2  47140  vonn0icc2  47142  smflimlem6  47226  ovmpordxf  48837  aacllem  50298