MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nffv Unicode version

Theorem nffv 5878
Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypotheses
Ref Expression
nffv.1
nffv.2
Assertion
Ref Expression
nffv

Proof of Theorem nffv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-fv 5601 . 2
2 nffv.2 . . . 4
3 nffv.1 . . . 4
4 nfcv 2619 . . . 4
52, 3, 4nfbr 4496 . . 3
65nfiota 5560 . 2
71, 6nfcxfr 2617 1
Colors of variables: wff setvar class
Syntax hints:  F/_wnfc 2605   class class class wbr 4452  iotacio 5554  `cfv 5593
This theorem is referenced by:  nffvmpt1  5879  nffvd  5880  dffn5f  5928  fvmptss  5964  fvmptex  5966  fvmptf  5972  fvmptnf  5973  eqfnfv2f  5985  ralrnmpt  6040  ffnfvf  6058  funiunfvf  6161  dff13f  6167  nfiso  6220  nfrecs  7063  nfrdg  7099  rdgsucmptf  7113  rdgsucmptnf  7114  frsucmpt  7122  frsucmptn  7123  rankidb  8239  rankval4  8306  dfac8clem  8434  cardaleph  8491  hsmexlem2  8828  axcc2  8838  uniimadomf  8941  nfseq  12117  seqof2  12165  rlim2  13319  nfsum1  13512  nfsum  13513  sumeq2ii  13515  fsumrelem  13621  o1fsum  13627  nfcprod1  13717  nfcprod  13718  fprodefsum  13830  prdsbas3  14878  prdsdsval2  14881  yonedalem4b  15545  gsum2d2lem  17001  coe1fzgsumdlem  18343  evl1gsumdlem  18392  ptcldmpt  20115  ptcnp  20123  cnmpt11  20164  cnmpt21  20172  cnmptk2  20187  prdsdsf  20870  prdsxmet  20872  ovolfiniun  21912  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  ovoliunnul  21918  volfiniun  21957  voliun  21964  mbfsup  22071  mbflim  22075  itg2splitlem  22155  itg2split  22156  itg2cnlem1  22168  isibl2  22173  nfitg1  22180  nfitg  22181  cbvitg  22182  itgabs  22241  dvlipcn  22395  lhop2  22416  dvfsumabs  22424  dvfsumrlim  22432  itgparts  22448  itgsubstlem  22449  ulmss  22792  itgulm2  22804  lgseisenlem2  23625  dchrisumlem3  23676  cnlnadjlem5  26990  dfimafnf  27473  esumfzf  28075  voliune  28201  volfiniune  28202  lgamgulmlem2  28572  lgamgulmlem6  28576  lgamgulm2  28578  cvmcov  28708  trpredlem1  29310  trpredrec  29321  nfwrecs  29338  sltval2  29416  nobndlem5  29456  itgabsnc  30084  mzpsubst  30681  aomclem8  31007  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  evth2f  31390  fvelrnbf  31393  evthf  31402  rfcnpre3  31408  rfcnpre4  31409  rfcnnnub  31411  refsum2cnlem1  31412  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fmul01lt1  31580  cncfmptss  31581  mulc1cncfg  31583  expcnfg  31586  fprodabs2  31602  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  idlimc  31632  limcperiod  31634  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  icccncfext  31690  cncficcgt0  31691  cncfiooicclem1  31696  dvnmul  31740  dvnprodlem1  31743  itgsubsticclem  31774  stoweidlem3  31785  stoweidlem23  31805  stoweidlem26  31808  stoweidlem28  31810  stoweidlem29  31811  stoweidlem31  31813  stoweidlem34  31816  stoweidlem36  31818  stoweidlem42  31824  stoweidlem48  31830  stoweidlem51  31833  stoweidlem52  31834  stoweidlem59  31841  wallispilem5  31851  stirlinglem4  31859  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  fourierdlem20  31909  fourierdlem31  31920  fourierdlem79  31968  fourierdlem89  31978  fourierdlem91  31980  fourierdlem112  32001  fourierdlem115  32004  fourierd  32005  fourierclimd  32006  etransclem2  32019  etransclem48  32065  nfafv  32221  bnj1534  33911  bnj1542  33915  bnj958  33998  bnj1000  33999  bnj1446  34101  bnj1447  34102  bnj1448  34103  bnj1466  34109  bnj1467  34110  bnj1519  34121  bnj1520  34122  bnj1529  34126  riotaocN  34934  cdleme32d  36170  cdleme32f  36172  ltrniotaval  36307  cdlemksv2  36573  cdlemkuv2  36593  cdlemk36  36639  cdlemk38  36641  cdlemk19x  36669  cdlemk11t  36672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator