Theorem nfov 7430

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

Syntax hints:  ⊤wtru 1564  Ⅎwnfc 2912  (class class class)co 7400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  csbov123  7444  ovmpos  7548  ov2gf  7549  ovmpodxf  7550  ovmpodv2  7558  ov3  7563  nfof  7670  offval2f  7679  offval2  7684  ofmpteq  7687  nffrecs  8268  oawordeulem  8527  nnawordex  8611  ttrcltr  9673  pwfseqlem2  10632  pwfseqlem4a  10634  pwfseqlem4  10635  nfseq  14035  rlim2  15535  fsumadd  15779  fsummulc2  15823  fsumrlim  15851  fprodmul  16002  fproddiv  16003  fproddivf  16029  pcmpt  16940  pcmptdvds  16942  prdsdsval2  17525  symgval  19429  gsum2d2  20032  gsumcom2  20033  prdsgsum  20039  dprd2d2  20104  gsumdixp  20388  pwsgprod  20399  evlslem4  22184  gsumply1eq  22426  madugsum  22757  cayleyhamilton1  23006  fiuncmp  23518  cnmpt2t  23787  cnmptcom  23792  cnmpt2k  23802  fsumcn  24986  ovoliunlem3  25620  isibl2  25882  nfitg1  25890  nfitg  25891  cbvitg  25892  itgfsum  25943  limciun  26010  dvmptfsum  26091  dvlipcn  26110  lhop2  26131  dvfsumabs  26139  dvfsumlem1  26142  dvfsumlem4  26145  dvfsum2  26150  itgparts  26163  itgsubstlem  26164  itgsubst  26165  elplyd  26316  coeeq2  26356  leibpi  27061  rlimcnp  27084  o1cxp  27093  dchrisumlem2  27608  dchrisumlem3  27609  nfseqs  28434  numclwlk2lem2f1o  30635  cnlnadjlem5  32328  iundisjf  32840  gsumpart  33291  suppgsumssiun  33300  gsumvsca1  33454  gsumvsca2  33455  rmfsupp2  33465  elrspunidl  33647  deg1prod  33785  nfesum1  34342  nfesum2  34343  esum2d  34395  ptrest  38125  sdclem1  38249  totbndbnd  38295  cdleme26ee  40991  cdleme31se2  41014  cdleme42b  41109  cdlemk11t  41577  dvdsrabdioph  43394  naddwordnexlem4  43985  binomcxplemdvbinom  44922  binomcxplemdvsum  44924  binomcxplemnotnn0  44925  rfcnpre1  45598  rfcnpre2  45610  iunmapss  45790  ssmapsn  45791  infrpgernmpt  46038  caucvgbf  46062  cvgcaule  46064  fsummulc1f  46146  mulc1cncfg  46164  expcnfg  46166  fprodexp  46169  climmulf  46179  climexp  46180  climsuse  46183  climrecf  46184  climaddf  46190  mullimc  46191  idlimc  46201  limcperiod  46203  addlimc  46221  0ellimcdiv  46222  climsubmpt  46233  fnlimabslt  46252  climuz  46317  limsupgt  46351  liminflt  46378  cncfshift  46447  dvmptmulf  46510  dvnmul  46516  dvmptfprodlem  46517  dvmptfprod  46518  stoweidlem23  46596  stoweidlem28  46601  stoweidlem36  46609  wallispilem5  46642  stirlinglem15  46661  fourierdlem20  46700  fourierdlem31  46711  fourierdlem68  46747  fourierdlem80  46759  fourierdlem86  46765  fourierdlem103  46782  fourierdlem104  46783  fourierdlem112  46791  fourierdlem115  46794  fourierd  46795  fourierclimd  46796  etransclem2  46809  sge0ltfirp  46973  sge0xaddlem2  47007  sge0xadd  47008  hoimbl2  47238  vonhoire  47245  vonioo  47255  vonicc  47258  vonn0ioo2  47263  vonn0icc2  47265  smflimlem6  47349  ovmpordxf  48971  aacllem  50431