Theorem nfov 7439

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  csbov123  7451  ovmpos  7556  ov2gf  7557  ovmpodxf  7558  ovmpodv2  7566  ov3  7570  nfof  7676  offval2f  7685  offval2  7690  ofmpteq  7692  nffrecs  8268  oawordeulem  8554  nnawordex  8637  ttrcltr  9711  pwfseqlem2  10654  pwfseqlem4a  10656  pwfseqlem4  10657  nfseq  13976  rlim2  15440  fsumadd  15686  fsummulc2  15730  fsumrlim  15757  fprodmul  15904  fproddiv  15905  fproddivf  15931  pcmpt  16825  pcmptdvds  16827  prdsdsval2  17430  symgval  19236  gsum2d2  19842  gsumcom2  19843  prdsgsum  19849  dprd2d2  19914  gsumdixp  20131  evlslem4  21637  gsumply1eq  21829  madugsum  22145  cayleyhamilton1  22394  fiuncmp  22908  cnmpt2t  23177  cnmptcom  23182  cnmpt2k  23192  fsumcn  24386  ovoliunlem3  25021  isibl2  25284  nfitg1  25291  nfitg  25292  cbvitg  25293  itgfsum  25344  limciun  25411  dvmptfsum  25492  dvlipcn  25511  lhop2  25532  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem4  25546  dvfsum2  25551  itgparts  25564  itgsubstlem  25565  itgsubst  25566  elplyd  25716  coeeq2  25756  leibpi  26447  rlimcnp  26470  o1cxp  26479  dchrisumlem2  26993  dchrisumlem3  26994  numclwlk2lem2f1o  29632  cnlnadjlem5  31324  iundisjf  31820  gsumpart  32207  gsumvsca1  32371  gsumvsca2  32372  rmfsupp2  32387  elrspunidl  32546  nfesum1  33038  nfesum2  33039  esum2d  33091  ptrest  36487  sdclem1  36611  totbndbnd  36657  cdleme26ee  39231  cdleme31se2  39254  cdleme42b  39349  cdlemk11t  39817  pwsgprod  41114  dvdsrabdioph  41548  naddwordnexlem4  42152  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  rfcnpre1  43703  rfcnpre2  43715  iunmapss  43914  ssmapsn  43915  infrpgernmpt  44175  caucvgbf  44200  cvgcaule  44202  fsummulc1f  44287  mulc1cncfg  44305  expcnfg  44307  fprodexp  44310  climmulf  44320  climexp  44321  climsuse  44324  climrecf  44325  climaddf  44331  mullimc  44332  idlimc  44342  limcperiod  44344  addlimc  44364  0ellimcdiv  44365  climsubmpt  44376  fnlimabslt  44395  climuz  44460  limsupgt  44494  liminflt  44521  cncfshift  44590  dvmptmulf  44653  dvnmul  44659  dvmptfprodlem  44660  dvmptfprod  44661  stoweidlem23  44739  stoweidlem28  44744  stoweidlem36  44752  wallispilem5  44785  stirlinglem15  44804  fourierdlem20  44843  fourierdlem31  44854  fourierdlem68  44890  fourierdlem80  44902  fourierdlem86  44908  fourierdlem103  44925  fourierdlem104  44926  fourierdlem112  44934  fourierdlem115  44937  fourierd  44938  fourierclimd  44939  etransclem2  44952  sge0ltfirp  45116  sge0xaddlem2  45150  sge0xadd  45151  hoimbl2  45381  vonhoire  45388  vonioo  45398  vonicc  45401  vonn0ioo2  45406  vonn0icc2  45408  smflimlem6  45492  ovmpordxf  47014  aacllem  47848