Theorem nfov 7461

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

Syntax hints:  ⊤wtru 1541  Ⅎwnfc 2890  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  csbov123  7475  ovmpos  7581  ov2gf  7582  ovmpodxf  7583  ovmpodv2  7591  ov3  7596  nfof  7703  offval2f  7712  offval2  7717  ofmpteq  7720  nffrecs  8308  oawordeulem  8592  nnawordex  8675  ttrcltr  9756  pwfseqlem2  10699  pwfseqlem4a  10701  pwfseqlem4  10702  nfseq  14052  rlim2  15532  fsumadd  15776  fsummulc2  15820  fsumrlim  15847  fprodmul  15996  fproddiv  15997  fproddivf  16023  pcmpt  16930  pcmptdvds  16932  prdsdsval2  17529  symgval  19388  gsum2d2  19992  gsumcom2  19993  prdsgsum  19999  dprd2d2  20064  gsumdixp  20316  evlslem4  22100  gsumply1eq  22313  madugsum  22649  cayleyhamilton1  22898  fiuncmp  23412  cnmpt2t  23681  cnmptcom  23686  cnmpt2k  23696  fsumcn  24894  ovoliunlem3  25539  isibl2  25801  nfitg1  25809  nfitg  25810  cbvitg  25811  itgfsum  25862  limciun  25929  dvmptfsum  26013  dvlipcn  26033  lhop2  26054  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem4  26070  dvfsum2  26075  itgparts  26088  itgsubstlem  26089  itgsubst  26090  elplyd  26241  coeeq2  26281  leibpi  26985  rlimcnp  27008  o1cxp  27018  dchrisumlem2  27534  dchrisumlem3  27535  nfseqs  28293  numclwlk2lem2f1o  30398  cnlnadjlem5  32090  iundisjf  32602  gsumpart  33060  gsumvsca1  33232  gsumvsca2  33233  rmfsupp2  33242  elrspunidl  33456  nfesum1  34041  nfesum2  34042  esum2d  34094  ptrest  37626  sdclem1  37750  totbndbnd  37796  cdleme26ee  40362  cdleme31se2  40385  cdleme42b  40480  cdlemk11t  40948  pwsgprod  42554  dvdsrabdioph  42821  naddwordnexlem4  43414  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  rfcnpre1  45024  rfcnpre2  45036  iunmapss  45220  ssmapsn  45221  infrpgernmpt  45476  caucvgbf  45500  cvgcaule  45502  fsummulc1f  45586  mulc1cncfg  45604  expcnfg  45606  fprodexp  45609  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climaddf  45630  mullimc  45631  idlimc  45641  limcperiod  45643  addlimc  45663  0ellimcdiv  45664  climsubmpt  45675  fnlimabslt  45694  climuz  45759  limsupgt  45793  liminflt  45820  cncfshift  45889  dvmptmulf  45952  dvnmul  45958  dvmptfprodlem  45959  dvmptfprod  45960  stoweidlem23  46038  stoweidlem28  46043  stoweidlem36  46051  wallispilem5  46084  stirlinglem15  46103  fourierdlem20  46142  fourierdlem31  46153  fourierdlem68  46189  fourierdlem80  46201  fourierdlem86  46207  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem115  46236  fourierd  46237  fourierclimd  46238  etransclem2  46251  sge0ltfirp  46415  sge0xaddlem2  46449  sge0xadd  46450  hoimbl2  46680  vonhoire  46687  vonioo  46697  vonicc  46700  vonn0ioo2  46705  vonn0icc2  46707  smflimlem6  46791  ovmpordxf  48255  aacllem  49320