Theorem nfov 7448

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421

This theorem is used by:  csbov123  7462  ovmpos  7566  ov2gf  7567  ovmpodxf  7568  ovmpodv2  7576  ov3  7581  nfof  7697  offval2f  7706  offval2  7711  ofmpteq  7714  nffrecs  8294  oawordeulem  8555  nnawordex  8639  ttrcltr  9710  pwfseqlem2  10737  pwfseqlem4a  10739  pwfseqlem4  10740  nfseq  14147  rlim2  15656  fsumadd  15899  fsummulc2  15943  fsumrlim  15971  fprodmul  16120  fproddiv  16121  fproddivf  16147  pcmpt  17063  pcmptdvds  17065  prdsdsval2  17648  symgval  19578  gsum2d2  20181  gsumcom2  20182  prdsgsum  20188  dprd2d2  20253  gsumdixp  20541  pwsgprod  20552  evlslem4  22378  gsumply1eq  22620  madugsum  22951  cayleyhamilton1  23203  fiuncmp  23715  cnmpt2t  23985  cnmptcom  23990  cnmpt2k  24000  fsumcn  25184  ovoliunlem3  25818  isibl2  26080  nfitg1  26087  nfitg  26088  cbvitg  26089  itgfsum  26140  limciun  26207  dvmptfsum  26288  dvlipcn  26307  lhop2  26328  dvfsumabs  26336  dvfsumlem1  26339  dvfsumlem4  26342  dvfsum2  26347  itgparts  26360  itgsubstlem  26361  itgsubst  26362  elplyd  26513  coeeq2  26554  leibpi  27263  rlimcnp  27286  o1cxp  27295  dchrisumlem2  27810  dchrisumlem3  27811  nfseqs  28666  numclwlk2lem2f1o  30973  cnlnadjlem5  32666  iundisjf  33176  gsumpart  33617  suppgsumssiun  33626  gsumvsca1  33780  gsumvsca2  33781  rmfsupp2  33791  elrspunidl  33971  deg1prod  34108  nfesum1  34665  nfesum2  34666  esum2d  34718  ptrest  38517  sdclem1  38657  totbndbnd  38703  cdleme26ee  41397  cdleme31se2  41420  cdleme42b  41515  cdlemk11t  41983  dvdsrabdioph  43796  naddwordnexlem4  44387  binomcxplemdvbinom  45322  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  rfcnpre1  46005  rfcnpre2  46017  iunmapss  46197  ssmapsn  46198  infrpgernmpt  46444  caucvgbf  46468  cvgcaule  46470  fsummulc1f  46552  mulc1cncfg  46570  expcnfg  46572  fprodexp  46575  climmulf  46585  climexp  46586  climsuse  46589  climrecf  46590  climaddf  46596  mullimc  46597  idlimc  46607  limcperiod  46609  addlimc  46627  0ellimcdiv  46628  climsubmpt  46639  fnlimabslt  46658  climuz  46723  limsupgt  46757  liminflt  46784  cncfshift  46853  dvmptmulf  46916  dvnmul  46922  dvmptfprodlem  46923  dvmptfprod  46924  stoweidlem23  47002  stoweidlem28  47007  stoweidlem36  47015  wallispilem5  47048  stirlinglem15  47067  fourierdlem20  47106  fourierdlem31  47117  fourierdlem68  47153  fourierdlem80  47165  fourierdlem86  47171  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  fourierdlem115  47200  fourierd  47201  fourierclimd  47202  etransclem2  47215  sge0ltfirp  47379  sge0xaddlem2  47413  sge0xadd  47414  hoimbl2  47644  vonhoire  47651  vonioo  47661  vonicc  47664  vonn0ioo2  47669  vonn0icc2  47671  smflimlem6  47755  ovmpordxf  49420  aacllem  50908