Theorem nfov 7478

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

Syntax hints:  ⊤wtru 1538  Ⅎwnfc 2893  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  csbov123  7492  ovmpos  7598  ov2gf  7599  ovmpodxf  7600  ovmpodv2  7608  ov3  7613  nfof  7720  offval2f  7729  offval2  7734  ofmpteq  7736  nffrecs  8324  oawordeulem  8610  nnawordex  8693  ttrcltr  9785  pwfseqlem2  10728  pwfseqlem4a  10730  pwfseqlem4  10731  nfseq  14062  rlim2  15542  fsumadd  15788  fsummulc2  15832  fsumrlim  15859  fprodmul  16008  fproddiv  16009  fproddivf  16035  pcmpt  16939  pcmptdvds  16941  prdsdsval2  17544  symgval  19412  gsum2d2  20016  gsumcom2  20017  prdsgsum  20023  dprd2d2  20088  gsumdixp  20342  evlslem4  22123  gsumply1eq  22334  madugsum  22670  cayleyhamilton1  22919  fiuncmp  23433  cnmpt2t  23702  cnmptcom  23707  cnmpt2k  23717  fsumcn  24913  ovoliunlem3  25558  isibl2  25821  nfitg1  25829  nfitg  25830  cbvitg  25831  itgfsum  25882  limciun  25949  dvmptfsum  26033  dvlipcn  26053  lhop2  26074  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem4  26090  dvfsum2  26095  itgparts  26108  itgsubstlem  26109  itgsubst  26110  elplyd  26261  coeeq2  26301  leibpi  27003  rlimcnp  27026  o1cxp  27036  dchrisumlem2  27552  dchrisumlem3  27553  nfseqs  28311  numclwlk2lem2f1o  30411  cnlnadjlem5  32103  iundisjf  32611  gsumpart  33038  gsumvsca1  33205  gsumvsca2  33206  rmfsupp2  33218  elrspunidl  33421  nfesum1  34004  nfesum2  34005  esum2d  34057  ptrest  37579  sdclem1  37703  totbndbnd  37749  cdleme26ee  40317  cdleme31se2  40340  cdleme42b  40435  cdlemk11t  40903  pwsgprod  42499  dvdsrabdioph  42766  naddwordnexlem4  43363  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  rfcnpre1  44919  rfcnpre2  44931  iunmapss  45122  ssmapsn  45123  infrpgernmpt  45380  caucvgbf  45405  cvgcaule  45407  fsummulc1f  45492  mulc1cncfg  45510  expcnfg  45512  fprodexp  45515  climmulf  45525  climexp  45526  climsuse  45529  climrecf  45530  climaddf  45536  mullimc  45537  idlimc  45547  limcperiod  45549  addlimc  45569  0ellimcdiv  45570  climsubmpt  45581  fnlimabslt  45600  climuz  45665  limsupgt  45699  liminflt  45726  cncfshift  45795  dvmptmulf  45858  dvnmul  45864  dvmptfprodlem  45865  dvmptfprod  45866  stoweidlem23  45944  stoweidlem28  45949  stoweidlem36  45957  wallispilem5  45990  stirlinglem15  46009  fourierdlem20  46048  fourierdlem31  46059  fourierdlem68  46095  fourierdlem80  46107  fourierdlem86  46113  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem115  46142  fourierd  46143  fourierclimd  46144  etransclem2  46157  sge0ltfirp  46321  sge0xaddlem2  46355  sge0xadd  46356  hoimbl2  46586  vonhoire  46593  vonioo  46603  vonicc  46606  vonn0ioo2  46611  vonn0icc2  46613  smflimlem6  46697  ovmpordxf  48063  aacllem  48895