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

Theorem nffv 5859
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  |-  F/_ x F
nffv.2  |-  F/_ x A
Assertion
Ref Expression
nffv  |-  F/_ x
( F `  A
)

Proof of Theorem nffv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-fv 5582 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2603 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4477 . . 3  |-  F/ x  A F y
65nfiota 5541 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2601 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2589   class class class wbr 4433   iotacio 5535   ` cfv 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582
This theorem is referenced by:  nffvmpt1  5860  nffvd  5861  dffn5f  5909  fvmptss  5945  fvmptex  5947  fvmptf  5953  fvmptnf  5954  eqfnfv2f  5966  ralrnmpt  6021  ffnfvf  6039  funiunfvf  6142  dff13f  6148  nfiso  6201  nfrecs  7042  nfrdg  7078  rdgsucmptf  7092  rdgsucmptnf  7093  frsucmpt  7101  frsucmptn  7102  rankidb  8216  rankval4  8283  dfac8clem  8411  cardaleph  8468  hsmexlem2  8805  axcc2  8815  uniimadomf  8918  nfseq  12091  seqof2  12139  rlim2  13293  nfsum1  13486  nfsum  13487  sumeq2ii  13489  fsumrelem  13595  o1fsum  13601  prdsbas3  14750  prdsdsval2  14753  yonedalem4b  15414  gsum2d2lem  16870  coe1fzgsumdlem  18211  evl1gsumdlem  18260  ptcldmpt  19981  ptcnp  19989  cnmpt11  20030  cnmpt21  20038  cnmptk2  20053  prdsdsf  20736  prdsxmet  20738  ovolfiniun  21778  ovoliunlem3  21781  ovoliun  21782  ovoliun2  21783  ovoliunnul  21784  volfiniun  21823  voliun  21830  mbfsup  21937  mbflim  21941  itg2splitlem  22021  itg2split  22022  itg2cnlem1  22034  isibl2  22039  nfitg1  22046  nfitg  22047  cbvitg  22048  itgabs  22107  dvlipcn  22261  lhop2  22282  dvfsumabs  22290  dvfsumrlim  22298  itgparts  22314  itgsubstlem  22315  ulmss  22657  itgulm2  22669  lgseisenlem2  23490  dchrisumlem3  23541  cnlnadjlem5  26855  dfimafnf  27338  esumfzf  27941  voliune  28067  volfiniune  28068  lgamgulmlem2  28438  lgamgulmlem6  28442  lgamgulm2  28444  cvmcov  28574  nfcprod1  29010  nfcprod  29011  fprodefsum  29072  trpredlem1  29278  trpredrec  29289  nfwrecs  29306  sltval2  29384  nobndlem5  29424  itgabsnc  30052  mzpsubst  30649  aomclem8  30975  evth2f  31337  fvelrnbf  31340  evthf  31349  rfcnpre3  31355  rfcnpre4  31356  rfcnnnub  31358  refsum2cnlem1  31359  fmul01  31498  fmuldfeqlem1  31500  fmuldfeq  31501  fmul01lt1lem1  31502  fmul01lt1lem2  31503  fmul01lt1  31504  cncfmptss  31505  mulc1cncfg  31507  expcnfg  31510  climmulf  31514  climexp  31515  climsuse  31518  climrecf  31519  climinff  31521  climaddf  31525  mullimc  31526  idlimc  31536  limcperiod  31538  neglimc  31557  addlimc  31558  0ellimcdiv  31559  cncfshift  31579  icccncfext  31593  cncficcgt0  31594  cncfiooicclem1  31599  itgsubsticclem  31660  stoweidlem3  31670  stoweidlem23  31690  stoweidlem26  31693  stoweidlem28  31695  stoweidlem29  31696  stoweidlem31  31698  stoweidlem34  31701  stoweidlem36  31703  stoweidlem42  31709  stoweidlem48  31715  stoweidlem51  31718  stoweidlem52  31719  stoweidlem59  31726  wallispilem5  31736  stirlinglem4  31744  stirlinglem11  31751  stirlinglem12  31752  stirlinglem13  31753  stirlinglem14  31754  stirlinglem15  31755  fourierdlem20  31794  fourierdlem31  31805  fourierdlem79  31853  fourierdlem89  31863  fourierdlem91  31865  fourierdlem112  31886  fourierdlem115  31889  fourierd  31890  fourierclimd  31891  nfafv  32055  bnj1534  33618  bnj1542  33622  bnj958  33705  bnj1000  33706  bnj1446  33808  bnj1447  33809  bnj1448  33810  bnj1466  33816  bnj1467  33817  bnj1519  33828  bnj1520  33829  bnj1529  33833  riotaocN  34636  cdleme32d  35872  cdleme32f  35874  ltrniotaval  36009  cdlemksv2  36275  cdlemkuv2  36295  cdlemk36  36341  cdlemk38  36343  cdlemk19x  36371  cdlemk11t  36374
  Copyright terms: Public domain W3C validator