Theorem nfov 7180

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

Syntax hints:  ⊤wtru 1534  Ⅎwnfc 2961  (class class class)co 7150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358  df-ov 7153

This theorem is referenced by:  csbov123  7192  ovmpos  7292  ov2gf  7293  ovmpodxf  7294  ovmpodv2  7302  ov3  7305  nfof  7408  offval2f  7415  offval2  7420  ofmpteq  7422  oawordeulem  8174  nnawordex  8257  pwfseqlem2  10075  pwfseqlem4a  10077  pwfseqlem4  10078  nfseq  13373  rlim2  14847  fsumadd  15090  fsummulc2  15133  fsumrlim  15160  fprodmul  15308  fproddiv  15309  fproddivf  15335  pcmpt  16222  pcmptdvds  16224  prdsdsval2  16751  symgval  18491  gsum2d2  19088  gsumcom2  19089  prdsgsum  19095  dprd2d2  19160  gsumdixp  19353  evlslem4  20282  gsumply1eq  20467  madugsum  21246  cayleyhamilton1  21494  fiuncmp  22006  cnmpt2t  22275  cnmptcom  22280  cnmpt2k  22290  fsumcn  23472  ovoliunlem3  24099  isibl2  24361  nfitg1  24368  nfitg  24369  cbvitg  24370  itgfsum  24421  limciun  24486  dvmptfsum  24566  dvlipcn  24585  lhop2  24606  dvfsumabs  24614  dvfsumlem1  24617  dvfsumlem4  24620  dvfsum2  24625  itgparts  24638  itgsubstlem  24639  itgsubst  24640  elplyd  24786  coeeq2  24826  leibpi  25514  rlimcnp  25537  o1cxp  25546  dchrisumlem2  26060  dchrisumlem3  26061  numclwlk2lem2f1o  28152  cnlnadjlem5  29842  iundisjf  30333  gsumvsca1  30849  gsumvsca2  30850  rmfsupp2  30861  nfesum1  31294  nfesum2  31295  esum2d  31347  nffrecs  33115  ptrest  34885  sdclem1  35012  totbndbnd  35061  cdleme26ee  37490  cdleme31se2  37513  cdleme42b  37608  cdlemk11t  38076  dvdsrabdioph  39400  binomcxplemdvbinom  40678  binomcxplemdvsum  40680  binomcxplemnotnn0  40681  rfcnpre1  41269  rfcnpre2  41281  iunmapss  41470  ssmapsn  41471  infrpgernmpt  41733  fsummulc1f  41843  mulc1cncfg  41862  expcnfg  41864  fprodexp  41867  climmulf  41877  climexp  41878  climsuse  41881  climrecf  41882  climaddf  41888  mullimc  41889  idlimc  41899  limcperiod  41901  addlimc  41921  0ellimcdiv  41922  climsubmpt  41933  fnlimabslt  41952  climuz  42017  limsupgt  42051  liminflt  42078  cncfshift  42149  dvmptmulf  42214  dvnmul  42220  dvmptfprodlem  42221  dvmptfprod  42222  stoweidlem23  42301  stoweidlem28  42306  stoweidlem36  42314  wallispilem5  42347  stirlinglem15  42366  fourierdlem20  42405  fourierdlem31  42416  fourierdlem68  42452  fourierdlem80  42464  fourierdlem86  42470  fourierdlem103  42487  fourierdlem104  42488  fourierdlem112  42496  fourierdlem115  42499  fourierd  42500  fourierclimd  42501  etransclem2  42514  sge0ltfirp  42675  sge0xaddlem2  42709  sge0xadd  42710  hoimbl2  42940  vonhoire  42947  vonioo  42957  vonicc  42960  vonn0ioo2  42965  vonn0icc2  42967  smflimlem6  43045  ovmpordxf  44380  aacllem  44895