Theorem nfov 7444

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

Syntax hints:  ⊤wtru 1535  Ⅎwnfc 2878  (class class class)co 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417

This theorem is referenced by:  csbov123  7456  ovmpos  7563  ov2gf  7564  ovmpodxf  7565  ovmpodv2  7573  ov3  7578  nfof  7685  offval2f  7694  offval2  7699  ofmpteq  7701  nffrecs  8282  oawordeulem  8568  nnawordex  8651  ttrcltr  9731  pwfseqlem2  10674  pwfseqlem4a  10676  pwfseqlem4  10677  nfseq  14000  rlim2  15464  fsumadd  15710  fsummulc2  15754  fsumrlim  15781  fprodmul  15928  fproddiv  15929  fproddivf  15955  pcmpt  16852  pcmptdvds  16854  prdsdsval2  17457  symgval  19314  gsum2d2  19920  gsumcom2  19921  prdsgsum  19927  dprd2d2  19992  gsumdixp  20244  evlslem4  22007  gsumply1eq  22215  madugsum  22532  cayleyhamilton1  22781  fiuncmp  23295  cnmpt2t  23564  cnmptcom  23569  cnmpt2k  23579  fsumcn  24775  ovoliunlem3  25420  isibl2  25683  nfitg1  25690  nfitg  25691  cbvitg  25692  itgfsum  25743  limciun  25810  dvmptfsum  25894  dvlipcn  25914  lhop2  25935  dvfsumabs  25944  dvfsumlem1  25947  dvfsumlem4  25951  dvfsum2  25956  itgparts  25969  itgsubstlem  25970  itgsubst  25971  elplyd  26123  coeeq2  26163  leibpi  26861  rlimcnp  26884  o1cxp  26894  dchrisumlem2  27410  dchrisumlem3  27411  nfseqs  28147  numclwlk2lem2f1o  30176  cnlnadjlem5  31868  iundisjf  32364  gsumpart  32747  gsumvsca1  32911  gsumvsca2  32912  rmfsupp2  32923  elrspunidl  33079  nfesum1  33595  nfesum2  33596  esum2d  33648  ptrest  37027  sdclem1  37151  totbndbnd  37197  cdleme26ee  39770  cdleme31se2  39793  cdleme42b  39888  cdlemk11t  40356  pwsgprod  41696  dvdsrabdioph  42152  naddwordnexlem4  42754  binomcxplemdvbinom  43713  binomcxplemdvsum  43715  binomcxplemnotnn0  43716  rfcnpre1  44304  rfcnpre2  44316  iunmapss  44511  ssmapsn  44512  infrpgernmpt  44770  caucvgbf  44795  cvgcaule  44797  fsummulc1f  44882  mulc1cncfg  44900  expcnfg  44902  fprodexp  44905  climmulf  44915  climexp  44916  climsuse  44919  climrecf  44920  climaddf  44926  mullimc  44927  idlimc  44937  limcperiod  44939  addlimc  44959  0ellimcdiv  44960  climsubmpt  44971  fnlimabslt  44990  climuz  45055  limsupgt  45089  liminflt  45116  cncfshift  45185  dvmptmulf  45248  dvnmul  45254  dvmptfprodlem  45255  dvmptfprod  45256  stoweidlem23  45334  stoweidlem28  45339  stoweidlem36  45347  wallispilem5  45380  stirlinglem15  45399  fourierdlem20  45438  fourierdlem31  45449  fourierdlem68  45485  fourierdlem80  45497  fourierdlem86  45503  fourierdlem103  45520  fourierdlem104  45521  fourierdlem112  45529  fourierdlem115  45532  fourierd  45533  fourierclimd  45534  etransclem2  45547  sge0ltfirp  45711  sge0xaddlem2  45745  sge0xadd  45746  hoimbl2  45976  vonhoire  45983  vonioo  45993  vonicc  45996  vonn0ioo2  46001  vonn0icc2  46003  smflimlem6  46087  ovmpordxf  47325  aacllem  48157