Theorem nfov 7460

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

Syntax hints:  ⊤wtru 1537  Ⅎwnfc 2887  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  csbov123  7474  ovmpos  7580  ov2gf  7581  ovmpodxf  7582  ovmpodv2  7590  ov3  7595  nfof  7702  offval2f  7711  offval2  7716  ofmpteq  7719  nffrecs  8306  oawordeulem  8590  nnawordex  8673  ttrcltr  9753  pwfseqlem2  10696  pwfseqlem4a  10698  pwfseqlem4  10699  nfseq  14048  rlim2  15528  fsumadd  15772  fsummulc2  15816  fsumrlim  15843  fprodmul  15992  fproddiv  15993  fproddivf  16019  pcmpt  16925  pcmptdvds  16927  prdsdsval2  17530  symgval  19402  gsum2d2  20006  gsumcom2  20007  prdsgsum  20013  dprd2d2  20078  gsumdixp  20332  evlslem4  22117  gsumply1eq  22328  madugsum  22664  cayleyhamilton1  22913  fiuncmp  23427  cnmpt2t  23696  cnmptcom  23701  cnmpt2k  23711  fsumcn  24907  ovoliunlem3  25552  isibl2  25815  nfitg1  25823  nfitg  25824  cbvitg  25825  itgfsum  25876  limciun  25943  dvmptfsum  26027  dvlipcn  26047  lhop2  26068  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem4  26084  dvfsum2  26089  itgparts  26102  itgsubstlem  26103  itgsubst  26104  elplyd  26255  coeeq2  26295  leibpi  26999  rlimcnp  27022  o1cxp  27032  dchrisumlem2  27548  dchrisumlem3  27549  nfseqs  28307  numclwlk2lem2f1o  30407  cnlnadjlem5  32099  iundisjf  32608  gsumpart  33042  gsumvsca1  33214  gsumvsca2  33215  rmfsupp2  33227  elrspunidl  33435  nfesum1  34020  nfesum2  34021  esum2d  34073  ptrest  37605  sdclem1  37729  totbndbnd  37775  cdleme26ee  40342  cdleme31se2  40365  cdleme42b  40460  cdlemk11t  40928  pwsgprod  42530  dvdsrabdioph  42797  naddwordnexlem4  43390  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  rfcnpre1  44956  rfcnpre2  44968  iunmapss  45157  ssmapsn  45158  infrpgernmpt  45414  caucvgbf  45439  cvgcaule  45441  fsummulc1f  45526  mulc1cncfg  45544  expcnfg  45546  fprodexp  45549  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climaddf  45570  mullimc  45571  idlimc  45581  limcperiod  45583  addlimc  45603  0ellimcdiv  45604  climsubmpt  45615  fnlimabslt  45634  climuz  45699  limsupgt  45733  liminflt  45760  cncfshift  45829  dvmptmulf  45892  dvnmul  45898  dvmptfprodlem  45899  dvmptfprod  45900  stoweidlem23  45978  stoweidlem28  45983  stoweidlem36  45991  wallispilem5  46024  stirlinglem15  46043  fourierdlem20  46082  fourierdlem31  46093  fourierdlem68  46129  fourierdlem80  46141  fourierdlem86  46147  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem115  46176  fourierd  46177  fourierclimd  46178  etransclem2  46191  sge0ltfirp  46355  sge0xaddlem2  46389  sge0xadd  46390  hoimbl2  46620  vonhoire  46627  vonioo  46637  vonicc  46640  vonn0ioo2  46645  vonn0icc2  46647  smflimlem6  46731  ovmpordxf  48183  aacllem  49031