Theorem nfov 7442

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

Syntax hints:  ⊤wtru 1571  Ⅎwnfc 2910  (class class class)co 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  csbov123  7456  ovmpos  7560  ov2gf  7561  ovmpodxf  7562  ovmpodv2  7570  ov3  7575  nfof  7682  offval2f  7691  offval2  7696  ofmpteq  7699  nffrecs  8281  oawordeulem  8540  nnawordex  8624  ttrcltr  9686  pwfseqlem2  10645  pwfseqlem4a  10647  pwfseqlem4  10648  nfseq  14049  rlim2  15549  fsumadd  15793  fsummulc2  15837  fsumrlim  15865  fprodmul  16016  fproddiv  16017  fproddivf  16043  pcmpt  16953  pcmptdvds  16955  prdsdsval2  17538  symgval  19442  gsum2d2  20045  gsumcom2  20046  prdsgsum  20052  dprd2d2  20117  gsumdixp  20401  pwsgprod  20412  evlslem4  22208  gsumply1eq  22450  madugsum  22781  cayleyhamilton1  23030  fiuncmp  23542  cnmpt2t  23811  cnmptcom  23816  cnmpt2k  23826  fsumcn  25010  ovoliunlem3  25644  isibl2  25906  nfitg1  25914  nfitg  25915  cbvitg  25916  itgfsum  25967  limciun  26034  dvmptfsum  26115  dvlipcn  26134  lhop2  26155  dvfsumabs  26163  dvfsumlem1  26166  dvfsumlem4  26169  dvfsum2  26174  itgparts  26187  itgsubstlem  26188  itgsubst  26189  elplyd  26340  coeeq2  26380  leibpi  27088  rlimcnp  27111  o1cxp  27120  dchrisumlem2  27635  dchrisumlem3  27636  nfseqs  28461  numclwlk2lem2f1o  30711  cnlnadjlem5  32404  iundisjf  32915  gsumpart  33364  suppgsumssiun  33373  gsumvsca1  33527  gsumvsca2  33528  rmfsupp2  33538  elrspunidl  33717  deg1prod  33854  nfesum1  34411  nfesum2  34412  esum2d  34464  ptrest  38251  sdclem1  38375  totbndbnd  38421  cdleme26ee  41115  cdleme31se2  41138  cdleme42b  41233  cdlemk11t  41701  dvdsrabdioph  43520  naddwordnexlem4  44111  binomcxplemdvbinom  45046  binomcxplemdvsum  45048  binomcxplemnotnn0  45049  rfcnpre1  45722  rfcnpre2  45734  iunmapss  45914  ssmapsn  45915  infrpgernmpt  46162  caucvgbf  46186  cvgcaule  46188  fsummulc1f  46270  mulc1cncfg  46288  expcnfg  46290  fprodexp  46293  climmulf  46303  climexp  46304  climsuse  46307  climrecf  46308  climaddf  46314  mullimc  46315  idlimc  46325  limcperiod  46327  addlimc  46345  0ellimcdiv  46346  climsubmpt  46357  fnlimabslt  46376  climuz  46441  limsupgt  46475  liminflt  46502  cncfshift  46571  dvmptmulf  46634  dvnmul  46640  dvmptfprodlem  46641  dvmptfprod  46642  stoweidlem23  46720  stoweidlem28  46725  stoweidlem36  46733  wallispilem5  46766  stirlinglem15  46785  fourierdlem20  46824  fourierdlem31  46835  fourierdlem68  46871  fourierdlem80  46883  fourierdlem86  46889  fourierdlem103  46906  fourierdlem104  46907  fourierdlem112  46915  fourierdlem115  46918  fourierd  46919  fourierclimd  46920  etransclem2  46933  sge0ltfirp  47097  sge0xaddlem2  47131  sge0xadd  47132  hoimbl2  47362  vonhoire  47369  vonioo  47379  vonicc  47382  vonn0ioo2  47387  vonn0icc2  47389  smflimlem6  47473  ovmpordxf  49102  aacllem  50584