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

Theorem nffv 5888
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 5609 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2591 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4470 . . 3  |-  F/ x  A F y
65nfiota 5569 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2589 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2577   class class class wbr 4426   iotacio 5563   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609
This theorem is referenced by:  nffvmpt1  5889  nffvd  5890  dffn5f  5936  fvmptss  5974  fvmptex  5976  fvmptf  5982  fvmptnf  5983  eqfnfv2f  5995  ralrnmpt  6046  ffnfvf  6065  funiunfvf  6169  dff13f  6175  nfiso  6230  nfwrecs  7038  nfrdg  7140  rdgsucmptf  7154  rdgsucmptnf  7155  frsucmpt  7163  frsucmptn  7164  rankidb  8270  rankval4  8337  dfac8clem  8461  cardaleph  8518  hsmexlem2  8855  axcc2  8865  uniimadomf  8968  nfseq  12220  seqof2  12268  rlim2  13538  nfsum1  13734  nfsum  13735  sumeq2ii  13737  fsumrelem  13845  o1fsum  13851  nfcprod1  13942  nfcprod  13943  fprodefsum  14127  prdsbas3  15338  prdsdsval2  15341  yonedalem4b  16112  gsum2d2lem  17540  coe1fzgsumdlem  18830  evl1gsumdlem  18879  ptcldmpt  20560  ptcnp  20568  cnmpt11  20609  cnmpt21  20617  cnmptk2  20632  prdsdsf  21313  prdsxmet  21315  ovolfiniun  22332  ovoliunlem3  22335  ovoliun  22336  ovoliun2  22337  ovoliunnul  22338  volfiniun  22377  voliun  22384  mbfsup  22497  mbflim  22503  itg2splitlem  22583  itg2split  22584  itg2cnlem1  22596  isibl2  22601  nfitg1  22608  nfitg  22609  cbvitg  22610  itgabs  22669  dvlipcn  22823  lhop2  22844  dvfsumabs  22852  dvfsumrlim  22860  itgparts  22876  itgsubstlem  22877  ulmss  23217  itgulm2  23229  lgamgulmlem2  23820  lgamgulmlem6  23824  lgamgulm2  23826  lgseisenlem2  24141  dchrisumlem3  24192  cnlnadjlem5  27559  dfimafnf  28073  esumfzf  28729  voliune  28891  volfiniune  28892  bnj1534  29452  bnj1542  29456  bnj958  29539  bnj1000  29540  bnj1446  29642  bnj1447  29643  bnj1448  29644  bnj1466  29650  bnj1467  29651  bnj1519  29662  bnj1520  29663  bnj1529  29667  cvmcov  29774  trpredlem1  30255  trpredrec  30266  sltval2  30330  nobndlem5  30370  poimirlem23  31667  poimirlem27  31671  itgabsnc  31715  riotaocN  32484  cdleme32d  33720  cdleme32f  33722  ltrniotaval  33857  cdlemksv2  34123  cdlemkuv2  34143  cdlemk36  34189  cdlemk38  34191  cdlemk19x  34219  cdlemk11t  34222  mzpsubst  35299  aomclem8  35625  binomcxplemdvbinom  36339  binomcxplemdvsum  36341  binomcxplemnotnn0  36342  evth2f  36976  fvelrnbf  36979  evthf  36988  rfcnpre3  36994  rfcnpre4  36995  rfcnnnub  36997  refsum2cnlem1  36998  dffo3f  37073  fmul01  37230  fmuldfeqlem1  37232  fmuldfeq  37233  fmul01lt1lem1  37234  fmul01lt1lem2  37235  fmul01lt1  37236  cncfmptss  37237  mulc1cncfg  37239  expcnfg  37243  fprodabs2  37247  climmulf  37254  climexp  37255  climsuse  37259  climrecf  37260  climinff  37262  climinffOLD  37263  climaddf  37267  mullimc  37268  idlimc  37278  limcperiod  37280  neglimc  37300  addlimc  37301  0ellimcdiv  37302  cncfshift  37323  icccncfext  37337  cncficcgt0  37338  cncfiooicclem1  37343  dvnmul  37387  dvnprodlem1  37390  itgsubsticclem  37421  stoweidlem3  37432  stoweidlem23  37452  stoweidlem26  37455  stoweidlem28  37457  stoweidlem29  37458  stoweidlem29OLD  37459  stoweidlem31  37461  stoweidlem34  37464  stoweidlem36  37466  stoweidlem42  37472  stoweidlem48  37478  stoweidlem51  37481  stoweidlem52  37482  stoweidlem59  37489  wallispilem5  37500  stirlinglem4  37508  stirlinglem11  37515  stirlinglem12  37516  stirlinglem13  37517  stirlinglem14  37518  stirlinglem15  37519  fourierdlem20  37558  fourierdlem31  37569  fourierdlem79  37617  fourierdlem89  37627  fourierdlem91  37629  fourierdlem112  37650  fourierdlem115  37653  fourierd  37654  fourierclimd  37655  etransclem2  37668  etransclem48  37714  sge0revalmpt  37754  sge0fsummpt  37766  sge0iunmptlemfi  37789  sge0iunmptlemre  37791  sge0iunmpt  37794  iundjiun  37807  meadjiun  37813  omeiunle  37847  omeiunltfirp  37849  nfafv  38037
  Copyright terms: Public domain W3C validator