Theorem nfov 7337

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

Syntax hints:  ⊤wtru 1540  Ⅎwnfc 2885  (class class class)co 7307

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310

This theorem is referenced by:  csbov123  7349  ovmpos  7453  ov2gf  7454  ovmpodxf  7455  ovmpodv2  7463  ov3  7467  nfof  7571  offval2f  7580  offval2  7585  ofmpteq  7587  nffrecs  8130  oawordeulem  8416  nnawordex  8499  ttrcltr  9518  pwfseqlem2  10461  pwfseqlem4a  10463  pwfseqlem4  10464  nfseq  13777  rlim2  15250  fsumadd  15497  fsummulc2  15541  fsumrlim  15568  fprodmul  15715  fproddiv  15716  fproddivf  15742  pcmpt  16638  pcmptdvds  16640  prdsdsval2  17240  symgval  19021  gsum2d2  19620  gsumcom2  19621  prdsgsum  19627  dprd2d2  19692  gsumdixp  19893  evlslem4  21329  gsumply1eq  21521  madugsum  21837  cayleyhamilton1  22086  fiuncmp  22600  cnmpt2t  22869  cnmptcom  22874  cnmpt2k  22884  fsumcn  24078  ovoliunlem3  24713  isibl2  24976  nfitg1  24983  nfitg  24984  cbvitg  24985  itgfsum  25036  limciun  25103  dvmptfsum  25184  dvlipcn  25203  lhop2  25224  dvfsumabs  25232  dvfsumlem1  25235  dvfsumlem4  25238  dvfsum2  25243  itgparts  25256  itgsubstlem  25257  itgsubst  25258  elplyd  25408  coeeq2  25448  leibpi  26137  rlimcnp  26160  o1cxp  26169  dchrisumlem2  26683  dchrisumlem3  26684  numclwlk2lem2f1o  28788  cnlnadjlem5  30478  iundisjf  30973  gsumpart  31360  gsumvsca1  31524  gsumvsca2  31525  rmfsupp2  31537  elrspunidl  31651  nfesum1  32053  nfesum2  32054  esum2d  32106  ptrest  35820  sdclem1  35945  totbndbnd  35991  cdleme26ee  38416  cdleme31se2  38439  cdleme42b  38534  cdlemk11t  39002  pwsgprod  40306  dvdsrabdioph  40669  binomcxplemdvbinom  42009  binomcxplemdvsum  42011  binomcxplemnotnn0  42012  rfcnpre1  42600  rfcnpre2  42612  iunmapss  42799  ssmapsn  42800  infrpgernmpt  43053  fsummulc1f  43161  mulc1cncfg  43179  expcnfg  43181  fprodexp  43184  climmulf  43194  climexp  43195  climsuse  43198  climrecf  43199  climaddf  43205  mullimc  43206  idlimc  43216  limcperiod  43218  addlimc  43238  0ellimcdiv  43239  climsubmpt  43250  fnlimabslt  43269  climuz  43334  limsupgt  43368  liminflt  43395  cncfshift  43464  dvmptmulf  43527  dvnmul  43533  dvmptfprodlem  43534  dvmptfprod  43535  stoweidlem23  43613  stoweidlem28  43618  stoweidlem36  43626  wallispilem5  43659  stirlinglem15  43678  fourierdlem20  43717  fourierdlem31  43728  fourierdlem68  43764  fourierdlem80  43776  fourierdlem86  43782  fourierdlem103  43799  fourierdlem104  43800  fourierdlem112  43808  fourierdlem115  43811  fourierd  43812  fourierclimd  43813  etransclem2  43826  sge0ltfirp  43988  sge0xaddlem2  44022  sge0xadd  44023  hoimbl2  44253  vonhoire  44260  vonioo  44270  vonicc  44273  vonn0ioo2  44278  vonn0icc2  44280  smflimlem6  44364  ovmpordxf  45732  aacllem  46563