Theorem nfov 7433

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

Syntax hints:  ⊤wtru 1541  Ⅎwnfc 2883  (class class class)co 7403

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  csbov123  7447  ovmpos  7553  ov2gf  7554  ovmpodxf  7555  ovmpodv2  7563  ov3  7568  nfof  7675  offval2f  7684  offval2  7689  ofmpteq  7692  nffrecs  8280  oawordeulem  8564  nnawordex  8647  ttrcltr  9728  pwfseqlem2  10671  pwfseqlem4a  10673  pwfseqlem4  10674  nfseq  14027  rlim2  15510  fsumadd  15754  fsummulc2  15798  fsumrlim  15825  fprodmul  15974  fproddiv  15975  fproddivf  16001  pcmpt  16910  pcmptdvds  16912  prdsdsval2  17496  symgval  19350  gsum2d2  19953  gsumcom2  19954  prdsgsum  19960  dprd2d2  20025  gsumdixp  20277  evlslem4  22032  gsumply1eq  22245  madugsum  22579  cayleyhamilton1  22828  fiuncmp  23340  cnmpt2t  23609  cnmptcom  23614  cnmpt2k  23624  fsumcn  24810  ovoliunlem3  25455  isibl2  25717  nfitg1  25725  nfitg  25726  cbvitg  25727  itgfsum  25778  limciun  25845  dvmptfsum  25929  dvlipcn  25949  lhop2  25970  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem4  25986  dvfsum2  25991  itgparts  26004  itgsubstlem  26005  itgsubst  26006  elplyd  26157  coeeq2  26197  leibpi  26902  rlimcnp  26925  o1cxp  26935  dchrisumlem2  27451  dchrisumlem3  27452  nfseqs  28210  numclwlk2lem2f1o  30306  cnlnadjlem5  31998  iundisjf  32516  gsumpart  32997  gsumvsca1  33169  gsumvsca2  33170  rmfsupp2  33179  elrspunidl  33389  nfesum1  34017  nfesum2  34018  esum2d  34070  ptrest  37589  sdclem1  37713  totbndbnd  37759  cdleme26ee  40325  cdleme31se2  40348  cdleme42b  40443  cdlemk11t  40911  pwsgprod  42514  dvdsrabdioph  42780  naddwordnexlem4  43372  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  rfcnpre1  44991  rfcnpre2  45003  iunmapss  45187  ssmapsn  45188  infrpgernmpt  45440  caucvgbf  45464  cvgcaule  45466  fsummulc1f  45548  mulc1cncfg  45566  expcnfg  45568  fprodexp  45571  climmulf  45581  climexp  45582  climsuse  45585  climrecf  45586  climaddf  45592  mullimc  45593  idlimc  45603  limcperiod  45605  addlimc  45625  0ellimcdiv  45626  climsubmpt  45637  fnlimabslt  45656  climuz  45721  limsupgt  45755  liminflt  45782  cncfshift  45851  dvmptmulf  45914  dvnmul  45920  dvmptfprodlem  45921  dvmptfprod  45922  stoweidlem23  46000  stoweidlem28  46005  stoweidlem36  46013  wallispilem5  46046  stirlinglem15  46065  fourierdlem20  46104  fourierdlem31  46115  fourierdlem68  46151  fourierdlem80  46163  fourierdlem86  46169  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem115  46198  fourierd  46199  fourierclimd  46200  etransclem2  46213  sge0ltfirp  46377  sge0xaddlem2  46411  sge0xadd  46412  hoimbl2  46642  vonhoire  46649  vonioo  46659  vonicc  46662  vonn0ioo2  46667  vonn0icc2  46669  smflimlem6  46753  ovmpordxf  48262  aacllem  49613