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

Theorem nffv 5894
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 5615 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2585 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4474 . . 3  |-  F/ x  A F y
65nfiota 5575 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2583 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2571   class class class wbr 4429   iotacio 5569   ` cfv 5607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3087  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-br 4430  df-iota 5571  df-fv 5615
This theorem is referenced by:  nffvmpt1  5895  nffvd  5896  dffn5f  5942  fvmptss  5980  fvmptex  5982  fvmptf  5988  fvmptnf  5989  eqfnfv2f  6001  ralrnmpt  6052  ffnfvf  6071  funiunfvf  6175  dff13f  6181  nfiso  6236  nfwrecs  7047  nfrdg  7149  rdgsucmptf  7163  rdgsucmptnf  7164  frsucmpt  7172  frsucmptn  7173  rankidb  8285  rankval4  8352  dfac8clem  8476  cardaleph  8533  hsmexlem2  8870  axcc2  8880  uniimadomf  8983  nfseq  12235  seqof2  12283  rlim2  13565  nfsum1  13761  nfsum  13762  sumeq2ii  13764  fsumrelem  13872  o1fsum  13878  nfcprod1  13969  nfcprod  13970  fprodefsum  14154  prdsbas3  15384  prdsdsval2  15387  yonedalem4b  16166  gsum2d2lem  17610  coe1fzgsumdlem  18900  evl1gsumdlem  18949  ptcldmpt  20633  ptcnp  20641  cnmpt11  20682  cnmpt21  20690  cnmptk2  20705  prdsdsf  21386  prdsxmet  21388  ovolfiniun  22458  ovoliunlem3  22461  ovoliun  22462  ovoliun2  22463  ovoliunnul  22464  volfiniun  22504  voliun  22511  mbfsup  22624  mbflim  22630  itg2splitlem  22710  itg2split  22711  itg2cnlem1  22723  isibl2  22728  nfitg1  22735  nfitg  22736  cbvitg  22737  itgabs  22796  dvlipcn  22950  lhop2  22971  dvfsumabs  22979  dvfsumrlim  22987  itgparts  23003  itgsubstlem  23004  ulmss  23356  itgulm2  23368  lgamgulmlem2  23959  lgamgulmlem6  23963  lgamgulm2  23965  lgseisenlem2  24282  dchrisumlem3  24333  cnlnadjlem5  27728  dfimafnf  28241  esumfzf  28904  voliune  29066  volfiniune  29067  bnj1534  29678  bnj1542  29682  bnj958  29765  bnj1000  29766  bnj1446  29868  bnj1447  29869  bnj1448  29870  bnj1466  29876  bnj1467  29877  bnj1519  29888  bnj1520  29889  bnj1529  29893  cvmcov  30000  trpredlem1  30481  trpredrec  30492  sltval2  30556  nobndlem5  30596  finxpreclem2  31752  finxpreclem6  31758  poimirlem23  31933  poimirlem27  31937  itgabsnc  31981  riotaocN  32750  cdleme32d  33986  cdleme32f  33988  ltrniotaval  34123  cdlemksv2  34389  cdlemkuv2  34409  cdlemk36  34455  cdlemk38  34457  cdlemk19x  34485  cdlemk11t  34488  mzpsubst  35565  aomclem8  35895  binomcxplemdvbinom  36678  binomcxplemdvsum  36680  binomcxplemnotnn0  36681  evth2f  37315  fvelrnbf  37318  evthf  37327  rfcnpre3  37333  rfcnpre4  37334  rfcnnnub  37336  refsum2cnlem1  37337  dffo3f  37417  fmul01  37604  fmuldfeqlem1  37606  fmuldfeq  37607  fmul01lt1lem1  37608  fmul01lt1lem2  37609  fmul01lt1  37610  cncfmptss  37611  mulc1cncfg  37613  expcnfg  37617  fprodabs2  37621  climmulf  37628  climexp  37629  climsuse  37633  climrecf  37634  climinff  37636  climinffOLD  37637  climaddf  37641  mullimc  37642  idlimc  37652  limcperiod  37654  neglimc  37674  addlimc  37675  0ellimcdiv  37676  cncfshift  37697  icccncfext  37711  cncficcgt0  37712  cncfiooicclem1  37717  dvnmul  37764  dvnprodlem1  37767  itgsubsticclem  37798  stoweidlem3  37809  stoweidlem23  37829  stoweidlem26  37832  stoweidlem28  37834  stoweidlem29  37835  stoweidlem29OLD  37836  stoweidlem31  37838  stoweidlem34  37841  stoweidlem36  37843  stoweidlem42  37849  stoweidlem48  37855  stoweidlem51  37858  stoweidlem52  37859  stoweidlem59  37866  wallispilem5  37877  stirlinglem4  37885  stirlinglem11  37892  stirlinglem12  37893  stirlinglem13  37894  stirlinglem14  37895  stirlinglem15  37896  fourierdlem20  37935  fourierdlem31  37946  fourierdlem31OLD  37947  fourierdlem79  37995  fourierdlem89  38005  fourierdlem91  38007  fourierdlem112  38028  fourierdlem115  38031  fourierd  38032  fourierclimd  38033  etransclem2  38047  etransclem48OLD  38093  etransclem48  38094  sge0revalmpt  38134  sge0fsummpt  38146  sge0iunmptlemfi  38169  sge0iunmptlemre  38171  sge0iunmpt  38174  sge0xadd  38191  sge0fsummptf  38192  sge0gtfsumgt  38199  iundjiun  38212  meadjiun  38218  omeiunle  38252  omeiunltfirp  38254  ovncvrrp  38296  nfafv  38514
  Copyright terms: Public domain W3C validator