Theorem nfov 7451

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnfc 2907  (class class class)co 7421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424

This theorem is used by:  csbov123  7465  ovmpos  7569  ov2gf  7570  ovmpodxf  7571  ovmpodv2  7579  ov3  7584  nfof  7700  offval2f  7709  offval2  7714  ofmpteq  7717  nffrecs  8305  oawordeulem  8566  nnawordex  8650  ttrcltr  9721  pwfseqlem2  10748  pwfseqlem4a  10750  pwfseqlem4  10751  nfseq  14158  rlim2  15669  fsumadd  15912  fsummulc2  15956  fsumrlim  15984  fprodmul  16133  fproddiv  16134  fproddivf  16160  pcmpt  17076  pcmptdvds  17078  prdsdsval2  17661  symgval  19591  gsum2d2  20194  gsumcom2  20195  prdsgsum  20201  dprd2d2  20266  gsumdixp  20554  pwsgprod  20565  evlslem4  22391  gsumply1eq  22633  madugsum  22964  cayleyhamilton1  23216  fiuncmp  23728  cnmpt2t  23998  cnmptcom  24003  cnmpt2k  24013  fsumcn  25197  ovoliunlem3  25831  isibl2  26093  nfitg1  26100  nfitg  26101  cbvitg  26102  itgfsum  26153  limciun  26220  dvmptfsum  26301  dvlipcn  26320  lhop2  26341  dvfsumabs  26349  dvfsumlem1  26352  dvfsumlem4  26355  dvfsum2  26360  itgparts  26373  itgsubstlem  26374  itgsubst  26375  elplyd  26526  coeeq2  26567  leibpi  27276  rlimcnp  27299  o1cxp  27308  dchrisumlem2  27823  dchrisumlem3  27824  nfseqs  28679  numclwlk2lem2f1o  30986  cnlnadjlem5  32679  iundisjf  33231  gsumpart  33671  suppgsumssiun  33680  gsumvsca1  33834  gsumvsca2  33835  rmfsupp2  33845  elrspunidl  34025  deg1prod  34162  nfesum1  34719  nfesum2  34720  esum2d  34772  ptrest  38631  sdclem1  38771  totbndbnd  38817  cdleme26ee  41511  cdleme31se2  41534  cdleme42b  41629  cdlemk11t  42097  dvdsrabdioph  43911  naddwordnexlem4  44497  binomcxplemdvbinom  45431  binomcxplemdvsum  45433  binomcxplemnotnn0  45434  rfcnpre1  46130  rfcnpre2  46142  iunmapss  46322  ssmapsn  46323  infrpgernmpt  46569  caucvgbf  46593  cvgcaule  46595  fsummulc1f  46677  mulc1cncfg  46695  expcnfg  46697  fprodexp  46700  climmulf  46710  climexp  46711  climsuse  46714  climrecf  46715  climaddf  46721  mullimc  46722  idlimc  46732  limcperiod  46734  addlimc  46752  0ellimcdiv  46753  climsubmpt  46764  fnlimabslt  46783  climuz  46848  limsupgt  46882  liminflt  46909  cncfshift  46978  dvmptmulf  47041  dvnmul  47047  dvmptfprodlem  47048  dvmptfprod  47049  stoweidlem23  47127  stoweidlem28  47132  stoweidlem36  47140  wallispilem5  47173  stirlinglem15  47192  fourierdlem20  47231  fourierdlem31  47242  fourierdlem68  47278  fourierdlem80  47290  fourierdlem86  47296  fourierdlem103  47313  fourierdlem104  47314  fourierdlem112  47322  fourierdlem115  47325  fourierd  47326  fourierclimd  47327  etransclem2  47340  sge0ltfirp  47504  sge0xaddlem2  47538  sge0xadd  47539  hoimbl2  47769  vonhoire  47776  vonioo  47786  vonicc  47789  vonn0ioo2  47794  vonn0icc2  47796  smflimlem6  47880  ovmpordxf  49545  aacllem  51108