Theorem nfov 7388

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

Syntax hints:  ⊤wtru 1542  Ⅎwnfc 2883  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  csbov123  7402  ovmpos  7506  ov2gf  7507  ovmpodxf  7508  ovmpodv2  7516  ov3  7521  nfof  7628  offval2f  7637  offval2  7642  ofmpteq  7645  nffrecs  8225  oawordeulem  8481  nnawordex  8565  ttrcltr  9625  pwfseqlem2  10570  pwfseqlem4a  10572  pwfseqlem4  10573  nfseq  13934  rlim2  15419  fsumadd  15663  fsummulc2  15707  fsumrlim  15734  fprodmul  15883  fproddiv  15884  fproddivf  15910  pcmpt  16820  pcmptdvds  16822  prdsdsval2  17404  symgval  19300  gsum2d2  19903  gsumcom2  19904  prdsgsum  19910  dprd2d2  19975  gsumdixp  20254  pwsgprod  20265  evlslem4  22031  gsumply1eq  22253  madugsum  22587  cayleyhamilton1  22836  fiuncmp  23348  cnmpt2t  23617  cnmptcom  23622  cnmpt2k  23632  fsumcn  24817  ovoliunlem3  25461  isibl2  25723  nfitg1  25731  nfitg  25732  cbvitg  25733  itgfsum  25784  limciun  25851  dvmptfsum  25935  dvlipcn  25955  lhop2  25976  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem4  25992  dvfsum2  25997  itgparts  26010  itgsubstlem  26011  itgsubst  26012  elplyd  26163  coeeq2  26203  leibpi  26908  rlimcnp  26931  o1cxp  26941  dchrisumlem2  27457  dchrisumlem3  27458  nfseqs  28283  numclwlk2lem2f1o  30454  cnlnadjlem5  32146  iundisjf  32664  gsumpart  33146  gsumvsca1  33308  gsumvsca2  33309  rmfsupp2  33320  elrspunidl  33509  deg1prod  33664  nfesum1  34197  nfesum2  34198  esum2d  34250  ptrest  37820  sdclem1  37944  totbndbnd  37990  cdleme26ee  40620  cdleme31se2  40643  cdleme42b  40738  cdlemk11t  41206  dvdsrabdioph  43052  naddwordnexlem4  43643  binomcxplemdvbinom  44594  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  rfcnpre1  45264  rfcnpre2  45276  iunmapss  45459  ssmapsn  45460  infrpgernmpt  45709  caucvgbf  45733  cvgcaule  45735  fsummulc1f  45817  mulc1cncfg  45835  expcnfg  45837  fprodexp  45840  climmulf  45850  climexp  45851  climsuse  45854  climrecf  45855  climaddf  45861  mullimc  45862  idlimc  45872  limcperiod  45874  addlimc  45892  0ellimcdiv  45893  climsubmpt  45904  fnlimabslt  45923  climuz  45988  limsupgt  46022  liminflt  46049  cncfshift  46118  dvmptmulf  46181  dvnmul  46187  dvmptfprodlem  46188  dvmptfprod  46189  stoweidlem23  46267  stoweidlem28  46272  stoweidlem36  46280  wallispilem5  46313  stirlinglem15  46332  fourierdlem20  46371  fourierdlem31  46382  fourierdlem68  46418  fourierdlem80  46430  fourierdlem86  46436  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem115  46465  fourierd  46466  fourierclimd  46467  etransclem2  46480  sge0ltfirp  46644  sge0xaddlem2  46678  sge0xadd  46679  hoimbl2  46909  vonhoire  46916  vonioo  46926  vonicc  46929  vonn0ioo2  46934  vonn0icc2  46936  smflimlem6  47020  ovmpordxf  48585  aacllem  50046