Theorem nfov 7383

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

Syntax hints:  ⊤wtru 1541  Ⅎwnfc 2876  (class class class)co 7353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  csbov123  7397  ovmpos  7501  ov2gf  7502  ovmpodxf  7503  ovmpodv2  7511  ov3  7516  nfof  7623  offval2f  7632  offval2  7637  ofmpteq  7640  nffrecs  8223  oawordeulem  8479  nnawordex  8562  ttrcltr  9631  pwfseqlem2  10572  pwfseqlem4a  10574  pwfseqlem4  10575  nfseq  13936  rlim2  15421  fsumadd  15665  fsummulc2  15709  fsumrlim  15736  fprodmul  15885  fproddiv  15886  fproddivf  15912  pcmpt  16822  pcmptdvds  16824  prdsdsval2  17406  symgval  19268  gsum2d2  19871  gsumcom2  19872  prdsgsum  19878  dprd2d2  19943  gsumdixp  20222  evlslem4  21999  gsumply1eq  22212  madugsum  22546  cayleyhamilton1  22795  fiuncmp  23307  cnmpt2t  23576  cnmptcom  23581  cnmpt2k  23591  fsumcn  24777  ovoliunlem3  25421  isibl2  25683  nfitg1  25691  nfitg  25692  cbvitg  25693  itgfsum  25744  limciun  25811  dvmptfsum  25895  dvlipcn  25915  lhop2  25936  dvfsumabs  25945  dvfsumlem1  25948  dvfsumlem4  25952  dvfsum2  25957  itgparts  25970  itgsubstlem  25971  itgsubst  25972  elplyd  26123  coeeq2  26163  leibpi  26868  rlimcnp  26891  o1cxp  26901  dchrisumlem2  27417  dchrisumlem3  27418  nfseqs  28204  numclwlk2lem2f1o  30341  cnlnadjlem5  32033  iundisjf  32551  gsumpart  33023  gsumvsca1  33181  gsumvsca2  33182  rmfsupp2  33191  elrspunidl  33378  nfesum1  34009  nfesum2  34010  esum2d  34062  ptrest  37601  sdclem1  37725  totbndbnd  37771  cdleme26ee  40342  cdleme31se2  40365  cdleme42b  40460  cdlemk11t  40928  pwsgprod  42520  dvdsrabdioph  42786  naddwordnexlem4  43377  binomcxplemdvbinom  44329  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  rfcnpre1  45000  rfcnpre2  45012  iunmapss  45196  ssmapsn  45197  infrpgernmpt  45448  caucvgbf  45472  cvgcaule  45474  fsummulc1f  45556  mulc1cncfg  45574  expcnfg  45576  fprodexp  45579  climmulf  45589  climexp  45590  climsuse  45593  climrecf  45594  climaddf  45600  mullimc  45601  idlimc  45611  limcperiod  45613  addlimc  45633  0ellimcdiv  45634  climsubmpt  45645  fnlimabslt  45664  climuz  45729  limsupgt  45763  liminflt  45790  cncfshift  45859  dvmptmulf  45922  dvnmul  45928  dvmptfprodlem  45929  dvmptfprod  45930  stoweidlem23  46008  stoweidlem28  46013  stoweidlem36  46021  wallispilem5  46054  stirlinglem15  46073  fourierdlem20  46112  fourierdlem31  46123  fourierdlem68  46159  fourierdlem80  46171  fourierdlem86  46177  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  fourierdlem115  46206  fourierd  46207  fourierclimd  46208  etransclem2  46221  sge0ltfirp  46385  sge0xaddlem2  46419  sge0xadd  46420  hoimbl2  46650  vonhoire  46657  vonioo  46667  vonicc  46670  vonn0ioo2  46675  vonn0icc2  46677  smflimlem6  46761  ovmpordxf  48327  aacllem  49790