Theorem nfov 6575

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 6574	. 2 ⊢ (⊤ → Ⅎ𝑥(𝐴𝐹𝐵))
8	7	trud 1484	1 ⊢ Ⅎ𝑥(𝐴𝐹𝐵)

Syntax hints:  ⊤wtru 1476  Ⅎwnfc 2738  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  csbov123  6585  ovmpt2s  6682  ov2gf  6683  ovmpt2dxf  6684  ovmpt2dv2  6692  ov3  6695  offval2f  6807  offval2  6812  ofmpteq  6814  oawordeulem  7521  nnawordex  7604  pwfseqlem2  9360  pwfseqlem4a  9362  pwfseqlem4  9363  nfseq  12673  rlim2  14075  fsumadd  14317  fsummulc2  14358  fsumrlim  14384  fprodmul  14529  fproddiv  14530  fproddivf  14557  pcmpt  15434  pcmptdvds  15436  prdsdsval2  15967  gsum2d2  18196  gsumcom2  18197  prdsgsum  18200  dprd2d2  18266  gsumdixp  18432  evlslem4  19329  gsumply1eq  19496  madugsum  20268  cayleyhamilton1  20516  fiuncmp  21017  cnmpt2t  21286  cnmptcom  21291  cnmpt2k  21301  fsumcn  22481  ovoliunlem3  23079  isibl2  23339  nfitg1  23346  nfitg  23347  cbvitg  23348  itgfsum  23399  limciun  23464  dvmptfsum  23542  dvlipcn  23561  lhop2  23582  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem4  23596  dvfsum2  23601  itgparts  23614  itgsubstlem  23615  itgsubst  23616  elplyd  23762  coeeq2  23802  leibpi  24469  rlimcnp  24492  o1cxp  24501  dchrisumlem2  24979  dchrisumlem3  24980  cnlnadjlem5  28314  iundisjf  28784  gsumvsca1  29113  gsumvsca2  29114  nfesum1  29429  nfesum2  29430  esum2d  29482  ptrest  32578  sdclem1  32709  totbndbnd  32758  cdleme26ee  34666  cdleme31se2  34689  cdleme42b  34784  cdlemk11t  35252  dvdsrabdioph  36392  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  rfcnpre1  38201  rfcnpre2  38213  iunmapss  38402  ssmapsn  38403  fsummulc1f  38635  mulc1cncfg  38656  expcnfg  38658  fprodexp  38661  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climaddf  38682  mullimc  38683  idlimc  38693  limcperiod  38695  addlimc  38715  0ellimcdiv  38716  climsubmpt  38727  fnlimabslt  38746  cncfshift  38759  dvmptmulf  38827  dvnmul  38833  dvmptfprodlem  38834  dvmptfprod  38835  stoweidlem23  38916  stoweidlem28  38921  stoweidlem36  38929  wallispilem5  38962  stirlinglem15  38981  fourierdlem20  39020  fourierdlem31  39031  fourierdlem68  39067  fourierdlem80  39079  fourierdlem86  39085  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem115  39114  fourierd  39115  fourierclimd  39116  etransclem2  39129  sge0ltfirp  39293  sge0xaddlem2  39327  sge0xadd  39328  hoimbl2  39555  vonhoire  39563  vonioo  39573  vonicc  39576  vonn0ioo2  39581  vonn0icc2  39583  smflimlem6  39662  ovmpt2rdxf  41910  aacllem  42356