Theorem nfov 7481

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnfc 2911  (class class class)co 7451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  csbov123  7495  ovmpos  7600  ov2gf  7601  ovmpodxf  7602  ovmpodv2  7610  ov3  7615  nfof  7731  offval2f  7740  offval2  7745  ofmpteq  7748  nffrecs  8339  oawordeulem  8600  nnawordex  8684  ttrcltr  9754  pwfseqlem2  10783  pwfseqlem4a  10785  pwfseqlem4  10786  nfseq  14194  rlim2  15707  fsumadd  15950  fsummulc2  15994  fsumrlim  16022  fprodmul  16171  fproddiv  16172  fproddivf  16198  pcmpt  17114  pcmptdvds  17116  prdsdsval2  17705  symgval  19636  gsum2d2  20239  gsumcom2  20240  prdsgsum  20246  dprd2d2  20311  gsumdixp  20599  pwsgprod  20610  evlslem4  22440  gsumply1eq  22682  madugsum  23013  cayleyhamilton1  23265  fiuncmp  23777  cnmpt2t  24047  cnmptcom  24052  cnmpt2k  24062  fsumcn  25246  ovoliunlem3  25880  isibl2  26142  nfitg1  26149  nfitg  26150  cbvitg  26151  itgfsum  26202  limciun  26269  dvmptfsum  26350  dvlipcn  26369  lhop2  26390  dvfsumabs  26398  dvfsumlem1  26401  dvfsumlem4  26404  dvfsum2  26409  itgparts  26422  itgsubstlem  26423  itgsubst  26424  elplyd  26575  coeeq2  26616  leibpi  27327  rlimcnp  27350  o1cxp  27359  dchrisumlem2  27874  dchrisumlem3  27875  nfseqs  28730  numclwlk2lem2f1o  31037  cnlnadjlem5  32730  iundisjf  33281  gsumpart  33723  suppgsumssiun  33732  gsumvsca1  33886  gsumvsca2  33887  rmfsupp2  33897  elrspunidl  34082  deg1prod  34218  nfesum1  34783  nfesum2  34784  esum2d  34836  ptrest  38805  sdclem1  38943  totbndbnd  38989  cdleme26ee  41683  cdleme31se2  41706  cdleme42b  41801  cdlemk11t  42269  dvdsrabdioph  44083  naddwordnexlem4  44664  binomcxplemdvbinom  45598  binomcxplemdvsum  45600  binomcxplemnotnn0  45601  rfcnpre1  46310  rfcnpre2  46322  iunmapss  46501  ssmapsn  46502  infrpgernmpt  46748  caucvgbf  46772  cvgcaule  46774  fsummulc1f  46856  mulc1cncfg  46874  expcnfg  46876  fprodexp  46879  climmulf  46889  climexp  46890  climsuse  46893  climrecf  46894  climaddf  46900  mullimc  46901  idlimc  46911  limcperiod  46913  addlimc  46931  0ellimcdiv  46932  climsubmpt  46943  fnlimabslt  46962  climuz  47027  limsupgt  47061  liminflt  47088  cncfshift  47157  dvmptmulf  47220  dvnmul  47226  dvmptfprodlem  47227  dvmptfprod  47228  stoweidlem23  47306  stoweidlem28  47311  stoweidlem36  47319  wallispilem5  47352  stirlinglem15  47371  fourierdlem20  47410  fourierdlem31  47421  fourierdlem68  47457  fourierdlem80  47469  fourierdlem86  47475  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  fourierdlem115  47504  fourierd  47505  fourierclimd  47506  etransclem2  47519  sge0ltfirp  47683  sge0xaddlem2  47717  sge0xadd  47718  hoimbl2  47948  vonhoire  47955  vonioo  47965  vonicc  47968  vonn0ioo2  47973  vonn0icc2  47975  smflimlem6  48059  ovmpordxf  49782  aacllem  51367