Theorem nfov 7443

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7416

This theorem is used by:  csbov123  7457  ovmpos  7561  ov2gf  7562  ovmpodxf  7563  ovmpodv2  7571  ov3  7576  nfof  7684  offval2f  7693  offval2  7698  ofmpteq  7701  nffrecs  8282  oawordeulem  8541  nnawordex  8625  ttrcltr  9695  pwfseqlem2  10668  pwfseqlem4a  10670  pwfseqlem4  10671  nfseq  14075  rlim2  15583  fsumadd  15826  fsummulc2  15870  fsumrlim  15898  fprodmul  16047  fproddiv  16048  fproddivf  16074  pcmpt  16984  pcmptdvds  16986  prdsdsval2  17569  symgval  19498  gsum2d2  20101  gsumcom2  20102  prdsgsum  20108  dprd2d2  20173  gsumdixp  20459  pwsgprod  20470  evlslem4  22292  gsumply1eq  22534  madugsum  22865  cayleyhamilton1  23117  fiuncmp  23629  cnmpt2t  23899  cnmptcom  23904  cnmpt2k  23914  fsumcn  25098  ovoliunlem3  25732  isibl2  25994  nfitg1  26001  nfitg  26002  cbvitg  26003  itgfsum  26054  limciun  26121  dvmptfsum  26202  dvlipcn  26221  lhop2  26242  dvfsumabs  26250  dvfsumlem1  26253  dvfsumlem4  26256  dvfsum2  26261  itgparts  26274  itgsubstlem  26275  itgsubst  26276  elplyd  26427  coeeq2  26468  leibpi  27179  rlimcnp  27202  o1cxp  27211  dchrisumlem2  27726  dchrisumlem3  27727  nfseqs  28552  numclwlk2lem2f1o  30859  cnlnadjlem5  32552  iundisjf  33062  gsumpart  33503  suppgsumssiun  33512  gsumvsca1  33666  gsumvsca2  33667  rmfsupp2  33677  elrspunidl  33856  deg1prod  33993  nfesum1  34550  nfesum2  34551  esum2d  34603  ptrest  38368  sdclem1  38493  totbndbnd  38539  cdleme26ee  41233  cdleme31se2  41256  cdleme42b  41351  cdlemk11t  41819  dvdsrabdioph  43651  naddwordnexlem4  44242  binomcxplemdvbinom  45177  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  rfcnpre1  45853  rfcnpre2  45865  iunmapss  46045  ssmapsn  46046  infrpgernmpt  46293  caucvgbf  46317  cvgcaule  46319  fsummulc1f  46401  mulc1cncfg  46419  expcnfg  46421  fprodexp  46424  climmulf  46434  climexp  46435  climsuse  46438  climrecf  46439  climaddf  46445  mullimc  46446  idlimc  46456  limcperiod  46458  addlimc  46476  0ellimcdiv  46477  climsubmpt  46488  fnlimabslt  46507  climuz  46572  limsupgt  46606  liminflt  46633  cncfshift  46702  dvmptmulf  46765  dvnmul  46771  dvmptfprodlem  46772  dvmptfprod  46773  stoweidlem23  46851  stoweidlem28  46856  stoweidlem36  46864  wallispilem5  46897  stirlinglem15  46916  fourierdlem20  46955  fourierdlem31  46966  fourierdlem68  47002  fourierdlem80  47014  fourierdlem86  47020  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  fourierdlem115  47049  fourierd  47050  fourierclimd  47051  etransclem2  47064  sge0ltfirp  47228  sge0xaddlem2  47262  sge0xadd  47263  hoimbl2  47493  vonhoire  47500  vonioo  47510  vonicc  47513  vonn0ioo2  47518  vonn0icc2  47520  smflimlem6  47604  ovmpordxf  49269  aacllem  50772