Theorem nfov 7298

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

Syntax hints:  ⊤wtru 1542  Ⅎwnfc 2888  (class class class)co 7268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  csbov123  7310  ovmpos  7412  ov2gf  7413  ovmpodxf  7414  ovmpodv2  7422  ov3  7426  nfof  7530  offval2f  7539  offval2  7544  ofmpteq  7546  nffrecs  8083  oawordeulem  8361  nnawordex  8444  ttrcltr  9435  pwfseqlem2  10399  pwfseqlem4a  10401  pwfseqlem4  10402  nfseq  13712  rlim2  15186  fsumadd  15433  fsummulc2  15477  fsumrlim  15504  fprodmul  15651  fproddiv  15652  fproddivf  15678  pcmpt  16574  pcmptdvds  16576  prdsdsval2  17176  symgval  18957  gsum2d2  19556  gsumcom2  19557  prdsgsum  19563  dprd2d2  19628  gsumdixp  19829  evlslem4  21265  gsumply1eq  21457  madugsum  21773  cayleyhamilton1  22022  fiuncmp  22536  cnmpt2t  22805  cnmptcom  22810  cnmpt2k  22820  fsumcn  24014  ovoliunlem3  24649  isibl2  24912  nfitg1  24919  nfitg  24920  cbvitg  24921  itgfsum  24972  limciun  25039  dvmptfsum  25120  dvlipcn  25139  lhop2  25160  dvfsumabs  25168  dvfsumlem1  25171  dvfsumlem4  25174  dvfsum2  25179  itgparts  25192  itgsubstlem  25193  itgsubst  25194  elplyd  25344  coeeq2  25384  leibpi  26073  rlimcnp  26096  o1cxp  26105  dchrisumlem2  26619  dchrisumlem3  26620  numclwlk2lem2f1o  28722  cnlnadjlem5  30412  iundisjf  30907  gsumpart  31294  gsumvsca1  31458  gsumvsca2  31459  rmfsupp2  31471  elrspunidl  31585  nfesum1  31987  nfesum2  31988  esum2d  32040  ptrest  35755  sdclem1  35880  totbndbnd  35926  cdleme26ee  38353  cdleme31se2  38376  cdleme42b  38471  cdlemk11t  38939  pwsgprod  40249  dvdsrabdioph  40612  binomcxplemdvbinom  41924  binomcxplemdvsum  41926  binomcxplemnotnn0  41927  rfcnpre1  42515  rfcnpre2  42527  iunmapss  42708  ssmapsn  42709  infrpgernmpt  42959  fsummulc1f  43066  mulc1cncfg  43084  expcnfg  43086  fprodexp  43089  climmulf  43099  climexp  43100  climsuse  43103  climrecf  43104  climaddf  43110  mullimc  43111  idlimc  43121  limcperiod  43123  addlimc  43143  0ellimcdiv  43144  climsubmpt  43155  fnlimabslt  43174  climuz  43239  limsupgt  43273  liminflt  43300  cncfshift  43369  dvmptmulf  43432  dvnmul  43438  dvmptfprodlem  43439  dvmptfprod  43440  stoweidlem23  43518  stoweidlem28  43523  stoweidlem36  43531  wallispilem5  43564  stirlinglem15  43583  fourierdlem20  43622  fourierdlem31  43633  fourierdlem68  43669  fourierdlem80  43681  fourierdlem86  43687  fourierdlem103  43704  fourierdlem104  43705  fourierdlem112  43713  fourierdlem115  43716  fourierd  43717  fourierclimd  43718  etransclem2  43731  sge0ltfirp  43892  sge0xaddlem2  43926  sge0xadd  43927  hoimbl2  44157  vonhoire  44164  vonioo  44174  vonicc  44177  vonn0ioo2  44182  vonn0icc2  44184  smflimlem6  44262  ovmpordxf  45626  aacllem  46457