Theorem nfov 7399

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  csbov123  7413  ovmpos  7517  ov2gf  7518  ovmpodxf  7519  ovmpodv2  7527  ov3  7532  nfof  7639  offval2f  7648  offval2  7653  ofmpteq  7656  nffrecs  8239  oawordeulem  8495  nnawordex  8578  ttrcltr  9645  pwfseqlem2  10588  pwfseqlem4a  10590  pwfseqlem4  10591  nfseq  13952  rlim2  15438  fsumadd  15682  fsummulc2  15726  fsumrlim  15753  fprodmul  15902  fproddiv  15903  fproddivf  15929  pcmpt  16839  pcmptdvds  16841  prdsdsval2  17423  symgval  19277  gsum2d2  19880  gsumcom2  19881  prdsgsum  19887  dprd2d2  19952  gsumdixp  20204  evlslem4  21959  gsumply1eq  22172  madugsum  22506  cayleyhamilton1  22755  fiuncmp  23267  cnmpt2t  23536  cnmptcom  23541  cnmpt2k  23551  fsumcn  24737  ovoliunlem3  25381  isibl2  25643  nfitg1  25651  nfitg  25652  cbvitg  25653  itgfsum  25704  limciun  25771  dvmptfsum  25855  dvlipcn  25875  lhop2  25896  dvfsumabs  25905  dvfsumlem1  25908  dvfsumlem4  25912  dvfsum2  25917  itgparts  25930  itgsubstlem  25931  itgsubst  25932  elplyd  26083  coeeq2  26123  leibpi  26828  rlimcnp  26851  o1cxp  26861  dchrisumlem2  27377  dchrisumlem3  27378  nfseqs  28157  numclwlk2lem2f1o  30281  cnlnadjlem5  31973  iundisjf  32491  gsumpart  32970  gsumvsca1  33152  gsumvsca2  33153  rmfsupp2  33162  elrspunidl  33372  nfesum1  34003  nfesum2  34004  esum2d  34056  ptrest  37586  sdclem1  37710  totbndbnd  37756  cdleme26ee  40327  cdleme31se2  40350  cdleme42b  40445  cdlemk11t  40913  pwsgprod  42505  dvdsrabdioph  42771  naddwordnexlem4  43363  binomcxplemdvbinom  44315  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  rfcnpre1  44986  rfcnpre2  44998  iunmapss  45182  ssmapsn  45183  infrpgernmpt  45434  caucvgbf  45458  cvgcaule  45460  fsummulc1f  45542  mulc1cncfg  45560  expcnfg  45562  fprodexp  45565  climmulf  45575  climexp  45576  climsuse  45579  climrecf  45580  climaddf  45586  mullimc  45587  idlimc  45597  limcperiod  45599  addlimc  45619  0ellimcdiv  45620  climsubmpt  45631  fnlimabslt  45650  climuz  45715  limsupgt  45749  liminflt  45776  cncfshift  45845  dvmptmulf  45908  dvnmul  45914  dvmptfprodlem  45915  dvmptfprod  45916  stoweidlem23  45994  stoweidlem28  45999  stoweidlem36  46007  wallispilem5  46040  stirlinglem15  46059  fourierdlem20  46098  fourierdlem31  46109  fourierdlem68  46145  fourierdlem80  46157  fourierdlem86  46163  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  fourierdlem115  46192  fourierd  46193  fourierclimd  46194  etransclem2  46207  sge0ltfirp  46371  sge0xaddlem2  46405  sge0xadd  46406  hoimbl2  46636  vonhoire  46643  vonioo  46653  vonicc  46656  vonn0ioo2  46661  vonn0icc2  46663  smflimlem6  46747  ovmpordxf  48300  aacllem  49763