Theorem nfov 7165

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

Syntax hints:  ⊤wtru 1539  Ⅎwnfc 2936  (class class class)co 7135

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  csbov123  7177  ovmpos  7277  ov2gf  7278  ovmpodxf  7279  ovmpodv2  7287  ov3  7291  nfof  7394  offval2f  7401  offval2  7406  ofmpteq  7408  oawordeulem  8163  nnawordex  8246  pwfseqlem2  10070  pwfseqlem4a  10072  pwfseqlem4  10073  nfseq  13374  rlim2  14845  fsumadd  15088  fsummulc2  15131  fsumrlim  15158  fprodmul  15306  fproddiv  15307  fproddivf  15333  pcmpt  16218  pcmptdvds  16220  prdsdsval2  16749  symgval  18489  gsum2d2  19087  gsumcom2  19088  prdsgsum  19094  dprd2d2  19159  gsumdixp  19355  evlslem4  20747  gsumply1eq  20934  madugsum  21248  cayleyhamilton1  21497  fiuncmp  22009  cnmpt2t  22278  cnmptcom  22283  cnmpt2k  22293  fsumcn  23475  ovoliunlem3  24108  isibl2  24370  nfitg1  24377  nfitg  24378  cbvitg  24379  itgfsum  24430  limciun  24497  dvmptfsum  24578  dvlipcn  24597  lhop2  24618  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem4  24632  dvfsum2  24637  itgparts  24650  itgsubstlem  24651  itgsubst  24652  elplyd  24799  coeeq2  24839  leibpi  25528  rlimcnp  25551  o1cxp  25560  dchrisumlem2  26074  dchrisumlem3  26075  numclwlk2lem2f1o  28164  cnlnadjlem5  29854  iundisjf  30352  gsumpart  30740  gsumvsca1  30904  gsumvsca2  30905  rmfsupp2  30917  elrspunidl  31014  nfesum1  31409  nfesum2  31410  esum2d  31462  nffrecs  33233  ptrest  35056  sdclem1  35181  totbndbnd  35227  cdleme26ee  37656  cdleme31se2  37679  cdleme42b  37774  cdlemk11t  38242  dvdsrabdioph  39751  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  rfcnpre1  41648  rfcnpre2  41660  iunmapss  41844  ssmapsn  41845  infrpgernmpt  42104  fsummulc1f  42212  mulc1cncfg  42231  expcnfg  42233  fprodexp  42236  climmulf  42246  climexp  42247  climsuse  42250  climrecf  42251  climaddf  42257  mullimc  42258  idlimc  42268  limcperiod  42270  addlimc  42290  0ellimcdiv  42291  climsubmpt  42302  fnlimabslt  42321  climuz  42386  limsupgt  42420  liminflt  42447  cncfshift  42516  dvmptmulf  42579  dvnmul  42585  dvmptfprodlem  42586  dvmptfprod  42587  stoweidlem23  42665  stoweidlem28  42670  stoweidlem36  42678  wallispilem5  42711  stirlinglem15  42730  fourierdlem20  42769  fourierdlem31  42780  fourierdlem68  42816  fourierdlem80  42828  fourierdlem86  42834  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem115  42863  fourierd  42864  fourierclimd  42865  etransclem2  42878  sge0ltfirp  43039  sge0xaddlem2  43073  sge0xadd  43074  hoimbl2  43304  vonhoire  43311  vonioo  43321  vonicc  43324  vonn0ioo2  43329  vonn0icc2  43331  smflimlem6  43409  ovmpordxf  44740  aacllem  45329