Theorem nfov 7299

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

Syntax hints:  ⊤wtru 1543  Ⅎwnfc 2889  (class class class)co 7269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-iota 6389  df-fv 6439  df-ov 7272

This theorem is referenced by:  csbov123  7311  ovmpos  7413  ov2gf  7414  ovmpodxf  7415  ovmpodv2  7423  ov3  7427  nfof  7531  offval2f  7540  offval2  7545  ofmpteq  7547  nffrecs  8088  oawordeulem  8368  nnawordex  8451  ttrcltr  9450  pwfseqlem2  10414  pwfseqlem4a  10416  pwfseqlem4  10417  nfseq  13727  rlim2  15201  fsumadd  15448  fsummulc2  15492  fsumrlim  15519  fprodmul  15666  fproddiv  15667  fproddivf  15693  pcmpt  16589  pcmptdvds  16591  prdsdsval2  17191  symgval  18972  gsum2d2  19571  gsumcom2  19572  prdsgsum  19578  dprd2d2  19643  gsumdixp  19844  evlslem4  21280  gsumply1eq  21472  madugsum  21788  cayleyhamilton1  22037  fiuncmp  22551  cnmpt2t  22820  cnmptcom  22825  cnmpt2k  22835  fsumcn  24029  ovoliunlem3  24664  isibl2  24927  nfitg1  24934  nfitg  24935  cbvitg  24936  itgfsum  24987  limciun  25054  dvmptfsum  25135  dvlipcn  25154  lhop2  25175  dvfsumabs  25183  dvfsumlem1  25186  dvfsumlem4  25189  dvfsum2  25194  itgparts  25207  itgsubstlem  25208  itgsubst  25209  elplyd  25359  coeeq2  25399  leibpi  26088  rlimcnp  26111  o1cxp  26120  dchrisumlem2  26634  dchrisumlem3  26635  numclwlk2lem2f1o  28737  cnlnadjlem5  30427  iundisjf  30922  gsumpart  31309  gsumvsca1  31473  gsumvsca2  31474  rmfsupp2  31486  elrspunidl  31600  nfesum1  32002  nfesum2  32003  esum2d  32055  ptrest  35770  sdclem1  35895  totbndbnd  35941  cdleme26ee  38368  cdleme31se2  38391  cdleme42b  38486  cdlemk11t  38954  pwsgprod  40264  dvdsrabdioph  40627  binomcxplemdvbinom  41939  binomcxplemdvsum  41941  binomcxplemnotnn0  41942  rfcnpre1  42530  rfcnpre2  42542  iunmapss  42723  ssmapsn  42724  infrpgernmpt  42974  fsummulc1f  43081  mulc1cncfg  43099  expcnfg  43101  fprodexp  43104  climmulf  43114  climexp  43115  climsuse  43118  climrecf  43119  climaddf  43125  mullimc  43126  idlimc  43136  limcperiod  43138  addlimc  43158  0ellimcdiv  43159  climsubmpt  43170  fnlimabslt  43189  climuz  43254  limsupgt  43288  liminflt  43315  cncfshift  43384  dvmptmulf  43447  dvnmul  43453  dvmptfprodlem  43454  dvmptfprod  43455  stoweidlem23  43533  stoweidlem28  43538  stoweidlem36  43546  wallispilem5  43579  stirlinglem15  43598  fourierdlem20  43637  fourierdlem31  43648  fourierdlem68  43684  fourierdlem80  43696  fourierdlem86  43702  fourierdlem103  43719  fourierdlem104  43720  fourierdlem112  43728  fourierdlem115  43731  fourierd  43732  fourierclimd  43733  etransclem2  43746  sge0ltfirp  43907  sge0xaddlem2  43941  sge0xadd  43942  hoimbl2  44172  vonhoire  44179  vonioo  44189  vonicc  44192  vonn0ioo2  44197  vonn0icc2  44199  smflimlem6  44277  ovmpordxf  45641  aacllem  46472