Theorem nfov 7417

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

Syntax hints:  ⊤wtru 1541  Ⅎwnfc 2876  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  csbov123  7431  ovmpos  7537  ov2gf  7538  ovmpodxf  7539  ovmpodv2  7547  ov3  7552  nfof  7659  offval2f  7668  offval2  7673  ofmpteq  7676  nffrecs  8262  oawordeulem  8518  nnawordex  8601  ttrcltr  9669  pwfseqlem2  10612  pwfseqlem4a  10614  pwfseqlem4  10615  nfseq  13976  rlim2  15462  fsumadd  15706  fsummulc2  15750  fsumrlim  15777  fprodmul  15926  fproddiv  15927  fproddivf  15953  pcmpt  16863  pcmptdvds  16865  prdsdsval2  17447  symgval  19301  gsum2d2  19904  gsumcom2  19905  prdsgsum  19911  dprd2d2  19976  gsumdixp  20228  evlslem4  21983  gsumply1eq  22196  madugsum  22530  cayleyhamilton1  22779  fiuncmp  23291  cnmpt2t  23560  cnmptcom  23565  cnmpt2k  23575  fsumcn  24761  ovoliunlem3  25405  isibl2  25667  nfitg1  25675  nfitg  25676  cbvitg  25677  itgfsum  25728  limciun  25795  dvmptfsum  25879  dvlipcn  25899  lhop2  25920  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem4  25936  dvfsum2  25941  itgparts  25954  itgsubstlem  25955  itgsubst  25956  elplyd  26107  coeeq2  26147  leibpi  26852  rlimcnp  26875  o1cxp  26885  dchrisumlem2  27401  dchrisumlem3  27402  nfseqs  28181  numclwlk2lem2f1o  30308  cnlnadjlem5  32000  iundisjf  32518  gsumpart  32997  gsumvsca1  33179  gsumvsca2  33180  rmfsupp2  33189  elrspunidl  33399  nfesum1  34030  nfesum2  34031  esum2d  34083  ptrest  37613  sdclem1  37737  totbndbnd  37783  cdleme26ee  40354  cdleme31se2  40377  cdleme42b  40472  cdlemk11t  40940  pwsgprod  42532  dvdsrabdioph  42798  naddwordnexlem4  43390  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  rfcnpre1  45013  rfcnpre2  45025  iunmapss  45209  ssmapsn  45210  infrpgernmpt  45461  caucvgbf  45485  cvgcaule  45487  fsummulc1f  45569  mulc1cncfg  45587  expcnfg  45589  fprodexp  45592  climmulf  45602  climexp  45603  climsuse  45606  climrecf  45607  climaddf  45613  mullimc  45614  idlimc  45624  limcperiod  45626  addlimc  45646  0ellimcdiv  45647  climsubmpt  45658  fnlimabslt  45677  climuz  45742  limsupgt  45776  liminflt  45803  cncfshift  45872  dvmptmulf  45935  dvnmul  45941  dvmptfprodlem  45942  dvmptfprod  45943  stoweidlem23  46021  stoweidlem28  46026  stoweidlem36  46034  wallispilem5  46067  stirlinglem15  46086  fourierdlem20  46125  fourierdlem31  46136  fourierdlem68  46172  fourierdlem80  46184  fourierdlem86  46190  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem115  46219  fourierd  46220  fourierclimd  46221  etransclem2  46234  sge0ltfirp  46398  sge0xaddlem2  46432  sge0xadd  46433  hoimbl2  46663  vonhoire  46670  vonioo  46680  vonicc  46683  vonn0ioo2  46688  vonn0icc2  46690  smflimlem6  46774  ovmpordxf  48327  aacllem  49790