Theorem nfov 7397

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

Syntax hints:  ⊤wtru 1543  Ⅎwnfc 2883  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  csbov123  7411  ovmpos  7515  ov2gf  7516  ovmpodxf  7517  ovmpodv2  7525  ov3  7530  nfof  7637  offval2f  7646  offval2  7651  ofmpteq  7654  nffrecs  8233  oawordeulem  8489  nnawordex  8573  ttrcltr  9637  pwfseqlem2  10582  pwfseqlem4a  10584  pwfseqlem4  10585  nfseq  13973  rlim2  15458  fsumadd  15702  fsummulc2  15746  fsumrlim  15774  fprodmul  15925  fproddiv  15926  fproddivf  15952  pcmpt  16863  pcmptdvds  16865  prdsdsval2  17447  symgval  19346  gsum2d2  19949  gsumcom2  19950  prdsgsum  19956  dprd2d2  20021  gsumdixp  20298  pwsgprod  20309  evlslem4  22054  gsumply1eq  22274  madugsum  22608  cayleyhamilton1  22857  fiuncmp  23369  cnmpt2t  23638  cnmptcom  23643  cnmpt2k  23653  fsumcn  24837  ovoliunlem3  25471  isibl2  25733  nfitg1  25741  nfitg  25742  cbvitg  25743  itgfsum  25794  limciun  25861  dvmptfsum  25942  dvlipcn  25961  lhop2  25982  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem4  25996  dvfsum2  26001  itgparts  26014  itgsubstlem  26015  itgsubst  26016  elplyd  26167  coeeq2  26207  leibpi  26906  rlimcnp  26929  o1cxp  26938  dchrisumlem2  27453  dchrisumlem3  27454  nfseqs  28279  numclwlk2lem2f1o  30449  cnlnadjlem5  32142  iundisjf  32659  gsumpart  33124  suppgsumssiun  33133  gsumvsca1  33287  gsumvsca2  33288  rmfsupp2  33299  elrspunidl  33488  deg1prod  33643  nfesum1  34184  nfesum2  34185  esum2d  34237  ptrest  37940  sdclem1  38064  totbndbnd  38110  cdleme26ee  40806  cdleme31se2  40829  cdleme42b  40924  cdlemk11t  41392  dvdsrabdioph  43238  naddwordnexlem4  43829  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  rfcnpre1  45450  rfcnpre2  45462  iunmapss  45644  ssmapsn  45645  infrpgernmpt  45893  caucvgbf  45917  cvgcaule  45919  fsummulc1f  46001  mulc1cncfg  46019  expcnfg  46021  fprodexp  46024  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climaddf  46045  mullimc  46046  idlimc  46056  limcperiod  46058  addlimc  46076  0ellimcdiv  46077  climsubmpt  46088  fnlimabslt  46107  climuz  46172  limsupgt  46206  liminflt  46233  cncfshift  46302  dvmptmulf  46365  dvnmul  46371  dvmptfprodlem  46372  dvmptfprod  46373  stoweidlem23  46451  stoweidlem28  46456  stoweidlem36  46464  wallispilem5  46497  stirlinglem15  46516  fourierdlem20  46555  fourierdlem31  46566  fourierdlem68  46602  fourierdlem80  46614  fourierdlem86  46620  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem115  46649  fourierd  46650  fourierclimd  46651  etransclem2  46664  sge0ltfirp  46828  sge0xaddlem2  46862  sge0xadd  46863  hoimbl2  47093  vonhoire  47100  vonioo  47110  vonicc  47113  vonn0ioo2  47118  vonn0icc2  47120  smflimlem6  47204  ovmpordxf  48815  aacllem  50276