Theorem nfov 7420

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

Syntax hints:  ⊤wtru 1560  Ⅎwnfc 2908  (class class class)co 7390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6471  df-fv 6523  df-ov 7393

This theorem is referenced by:  csbov123  7434  ovmpos  7538  ov2gf  7539  ovmpodxf  7540  ovmpodv2  7548  ov3  7553  nfof  7660  offval2f  7669  offval2  7674  ofmpteq  7677  nffrecs  8257  oawordeulem  8516  nnawordex  8600  ttrcltr  9664  pwfseqlem2  10610  pwfseqlem4a  10612  pwfseqlem4  10613  nfseq  14017  rlim2  15513  fsumadd  15757  fsummulc2  15801  fsumrlim  15829  fprodmul  15980  fproddiv  15981  fproddivf  16007  pcmpt  16918  pcmptdvds  16920  prdsdsval2  17503  symgval  19401  gsum2d2  20004  gsumcom2  20005  prdsgsum  20011  dprd2d2  20076  gsumdixp  20353  pwsgprod  20364  evlslem4  22116  gsumply1eq  22359  madugsum  22690  cayleyhamilton1  22939  fiuncmp  23451  cnmpt2t  23720  cnmptcom  23725  cnmpt2k  23735  fsumcn  24919  ovoliunlem3  25553  isibl2  25815  nfitg1  25823  nfitg  25824  cbvitg  25825  itgfsum  25876  limciun  25943  dvmptfsum  26024  dvlipcn  26043  lhop2  26064  dvfsumabs  26072  dvfsumlem1  26075  dvfsumlem4  26078  dvfsum2  26083  itgparts  26096  itgsubstlem  26097  itgsubst  26098  elplyd  26249  coeeq2  26289  leibpi  26994  rlimcnp  27017  o1cxp  27026  dchrisumlem2  27541  dchrisumlem3  27542  nfseqs  28367  numclwlk2lem2f1o  30537  cnlnadjlem5  32230  iundisjf  32748  gsumpart  33203  suppgsumssiun  33212  gsumvsca1  33366  gsumvsca2  33367  rmfsupp2  33378  elrspunidl  33574  deg1prod  33739  nfesum1  34297  nfesum2  34298  esum2d  34350  ptrest  38078  sdclem1  38202  totbndbnd  38248  cdleme26ee  40944  cdleme31se2  40967  cdleme42b  41062  cdlemk11t  41530  dvdsrabdioph  43347  naddwordnexlem4  43938  binomcxplemdvbinom  44889  binomcxplemdvsum  44891  binomcxplemnotnn0  44892  rfcnpre1  45559  rfcnpre2  45571  iunmapss  45751  ssmapsn  45752  infrpgernmpt  45999  caucvgbf  46023  cvgcaule  46025  fsummulc1f  46107  mulc1cncfg  46125  expcnfg  46127  fprodexp  46130  climmulf  46140  climexp  46141  climsuse  46144  climrecf  46145  climaddf  46151  mullimc  46152  idlimc  46162  limcperiod  46164  addlimc  46182  0ellimcdiv  46183  climsubmpt  46194  fnlimabslt  46213  climuz  46278  limsupgt  46312  liminflt  46339  cncfshift  46408  dvmptmulf  46471  dvnmul  46477  dvmptfprodlem  46478  dvmptfprod  46479  stoweidlem23  46557  stoweidlem28  46562  stoweidlem36  46570  wallispilem5  46603  stirlinglem15  46622  fourierdlem20  46661  fourierdlem31  46672  fourierdlem68  46708  fourierdlem80  46720  fourierdlem86  46726  fourierdlem103  46743  fourierdlem104  46744  fourierdlem112  46752  fourierdlem115  46755  fourierd  46756  fourierclimd  46757  etransclem2  46770  sge0ltfirp  46934  sge0xaddlem2  46968  sge0xadd  46969  hoimbl2  47199  vonhoire  47206  vonioo  47216  vonicc  47219  vonn0ioo2  47224  vonn0icc2  47226  smflimlem6  47310  ovmpordxf  48921  aacllem  50382