Theorem nfov 7420

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

Syntax hints:  ⊤wtru 1541  Ⅎwnfc 2877  (class class class)co 7390

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  csbov123  7434  ovmpos  7540  ov2gf  7541  ovmpodxf  7542  ovmpodv2  7550  ov3  7555  nfof  7662  offval2f  7671  offval2  7676  ofmpteq  7679  nffrecs  8265  oawordeulem  8521  nnawordex  8604  ttrcltr  9676  pwfseqlem2  10619  pwfseqlem4a  10621  pwfseqlem4  10622  nfseq  13983  rlim2  15469  fsumadd  15713  fsummulc2  15757  fsumrlim  15784  fprodmul  15933  fproddiv  15934  fproddivf  15960  pcmpt  16870  pcmptdvds  16872  prdsdsval2  17454  symgval  19308  gsum2d2  19911  gsumcom2  19912  prdsgsum  19918  dprd2d2  19983  gsumdixp  20235  evlslem4  21990  gsumply1eq  22203  madugsum  22537  cayleyhamilton1  22786  fiuncmp  23298  cnmpt2t  23567  cnmptcom  23572  cnmpt2k  23582  fsumcn  24768  ovoliunlem3  25412  isibl2  25674  nfitg1  25682  nfitg  25683  cbvitg  25684  itgfsum  25735  limciun  25802  dvmptfsum  25886  dvlipcn  25906  lhop2  25927  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem4  25943  dvfsum2  25948  itgparts  25961  itgsubstlem  25962  itgsubst  25963  elplyd  26114  coeeq2  26154  leibpi  26859  rlimcnp  26882  o1cxp  26892  dchrisumlem2  27408  dchrisumlem3  27409  nfseqs  28188  numclwlk2lem2f1o  30315  cnlnadjlem5  32007  iundisjf  32525  gsumpart  33004  gsumvsca1  33186  gsumvsca2  33187  rmfsupp2  33196  elrspunidl  33406  nfesum1  34037  nfesum2  34038  esum2d  34090  ptrest  37620  sdclem1  37744  totbndbnd  37790  cdleme26ee  40361  cdleme31se2  40384  cdleme42b  40479  cdlemk11t  40947  pwsgprod  42539  dvdsrabdioph  42805  naddwordnexlem4  43397  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  rfcnpre1  45020  rfcnpre2  45032  iunmapss  45216  ssmapsn  45217  infrpgernmpt  45468  caucvgbf  45492  cvgcaule  45494  fsummulc1f  45576  mulc1cncfg  45594  expcnfg  45596  fprodexp  45599  climmulf  45609  climexp  45610  climsuse  45613  climrecf  45614  climaddf  45620  mullimc  45621  idlimc  45631  limcperiod  45633  addlimc  45653  0ellimcdiv  45654  climsubmpt  45665  fnlimabslt  45684  climuz  45749  limsupgt  45783  liminflt  45810  cncfshift  45879  dvmptmulf  45942  dvnmul  45948  dvmptfprodlem  45949  dvmptfprod  45950  stoweidlem23  46028  stoweidlem28  46033  stoweidlem36  46041  wallispilem5  46074  stirlinglem15  46093  fourierdlem20  46132  fourierdlem31  46143  fourierdlem68  46179  fourierdlem80  46191  fourierdlem86  46197  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem115  46226  fourierd  46227  fourierclimd  46228  etransclem2  46241  sge0ltfirp  46405  sge0xaddlem2  46439  sge0xadd  46440  hoimbl2  46670  vonhoire  46677  vonioo  46687  vonicc  46690  vonn0ioo2  46695  vonn0icc2  46697  smflimlem6  46781  ovmpordxf  48331  aacllem  49794