Theorem nfov 7398

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  csbov123  7412  ovmpos  7516  ov2gf  7517  ovmpodxf  7518  ovmpodv2  7526  ov3  7531  nfof  7638  offval2f  7647  offval2  7652  ofmpteq  7655  nffrecs  8235  oawordeulem  8491  nnawordex  8575  ttrcltr  9637  pwfseqlem2  10582  pwfseqlem4a  10584  pwfseqlem4  10585  nfseq  13946  rlim2  15431  fsumadd  15675  fsummulc2  15719  fsumrlim  15746  fprodmul  15895  fproddiv  15896  fproddivf  15922  pcmpt  16832  pcmptdvds  16834  prdsdsval2  17416  symgval  19312  gsum2d2  19915  gsumcom2  19916  prdsgsum  19922  dprd2d2  19987  gsumdixp  20266  pwsgprod  20277  evlslem4  22043  gsumply1eq  22265  madugsum  22599  cayleyhamilton1  22848  fiuncmp  23360  cnmpt2t  23629  cnmptcom  23634  cnmpt2k  23644  fsumcn  24829  ovoliunlem3  25473  isibl2  25735  nfitg1  25743  nfitg  25744  cbvitg  25745  itgfsum  25796  limciun  25863  dvmptfsum  25947  dvlipcn  25967  lhop2  25988  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem4  26004  dvfsum2  26009  itgparts  26022  itgsubstlem  26023  itgsubst  26024  elplyd  26175  coeeq2  26215  leibpi  26920  rlimcnp  26943  o1cxp  26953  dchrisumlem2  27469  dchrisumlem3  27470  nfseqs  28295  numclwlk2lem2f1o  30466  cnlnadjlem5  32158  iundisjf  32675  gsumpart  33156  suppgsumssiun  33165  gsumvsca1  33319  gsumvsca2  33320  rmfsupp2  33331  elrspunidl  33520  deg1prod  33675  nfesum1  34217  nfesum2  34218  esum2d  34270  ptrest  37867  sdclem1  37991  totbndbnd  38037  cdleme26ee  40733  cdleme31se2  40756  cdleme42b  40851  cdlemk11t  41319  dvdsrabdioph  43164  naddwordnexlem4  43755  binomcxplemdvbinom  44706  binomcxplemdvsum  44708  binomcxplemnotnn0  44709  rfcnpre1  45376  rfcnpre2  45388  iunmapss  45570  ssmapsn  45571  infrpgernmpt  45820  caucvgbf  45844  cvgcaule  45846  fsummulc1f  45928  mulc1cncfg  45946  expcnfg  45948  fprodexp  45951  climmulf  45961  climexp  45962  climsuse  45965  climrecf  45966  climaddf  45972  mullimc  45973  idlimc  45983  limcperiod  45985  addlimc  46003  0ellimcdiv  46004  climsubmpt  46015  fnlimabslt  46034  climuz  46099  limsupgt  46133  liminflt  46160  cncfshift  46229  dvmptmulf  46292  dvnmul  46298  dvmptfprodlem  46299  dvmptfprod  46300  stoweidlem23  46378  stoweidlem28  46383  stoweidlem36  46391  wallispilem5  46424  stirlinglem15  46443  fourierdlem20  46482  fourierdlem31  46493  fourierdlem68  46529  fourierdlem80  46541  fourierdlem86  46547  fourierdlem103  46564  fourierdlem104  46565  fourierdlem112  46573  fourierdlem115  46576  fourierd  46577  fourierclimd  46578  etransclem2  46591  sge0ltfirp  46755  sge0xaddlem2  46789  sge0xadd  46790  hoimbl2  47020  vonhoire  47027  vonioo  47037  vonicc  47040  vonn0ioo2  47045  vonn0icc2  47047  smflimlem6  47131  ovmpordxf  48696  aacllem  50157