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

Theorem nffv 5895
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 2603 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4461 . . 3  |-  F/ x  A F y
65nfiota 5569 . 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 2590   class class class wbr 4416   iotacio 5563   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609
This theorem is referenced by:  nffvmpt1  5896  nffvd  5897  dffn5f  5943  fvmptss  5981  fvmptex  5983  fvmptf  5989  fvmptnf  5990  eqfnfv2f  6003  ralrnmpt  6054  ffnfvf  6073  funiunfvf  6179  dff13f  6185  nfiso  6240  nfwrecs  7056  nfrdg  7158  rdgsucmptf  7172  rdgsucmptnf  7173  frsucmpt  7181  frsucmptn  7182  rankidb  8297  rankval4  8364  dfac8clem  8489  cardaleph  8546  hsmexlem2  8883  axcc2  8893  uniimadomf  8996  nfseq  12255  seqof2  12303  rlim2  13609  nfsum1  13805  nfsum  13806  sumeq2ii  13808  fsumrelem  13916  o1fsum  13922  nfcprod1  14013  nfcprod  14014  fprodefsum  14198  prdsbas3  15428  prdsdsval2  15431  yonedalem4b  16210  gsum2d2lem  17654  coe1fzgsumdlem  18944  evl1gsumdlem  18993  ptcldmpt  20678  ptcnp  20686  cnmpt11  20727  cnmpt21  20735  cnmptk2  20750  prdsdsf  21431  prdsxmet  21433  ovolfiniun  22503  ovoliunlem3  22506  ovoliun  22507  ovoliun2  22508  ovoliunnul  22509  volfiniun  22549  voliun  22556  mbfsup  22669  mbflim  22675  itg2splitlem  22755  itg2split  22756  itg2cnlem1  22768  isibl2  22773  nfitg1  22780  nfitg  22781  cbvitg  22782  itgabs  22841  dvlipcn  22995  lhop2  23016  dvfsumabs  23024  dvfsumrlim  23032  itgparts  23048  itgsubstlem  23049  ulmss  23401  itgulm2  23413  lgamgulmlem2  24004  lgamgulmlem6  24008  lgamgulm2  24010  lgseisenlem2  24327  dchrisumlem3  24378  cnlnadjlem5  27773  dfimafnf  28282  esumfzf  28939  voliune  29101  volfiniune  29102  bnj1534  29713  bnj1542  29717  bnj958  29800  bnj1000  29801  bnj1446  29903  bnj1447  29904  bnj1448  29905  bnj1466  29911  bnj1467  29912  bnj1519  29923  bnj1520  29924  bnj1529  29928  cvmcov  30035  trpredlem1  30517  trpredrec  30528  sltval2  30592  nobndlem5  30634  finxpreclem2  31827  finxpreclem6  31833  poimirlem23  32008  poimirlem27  32012  itgabsnc  32056  riotaocN  32820  cdleme32d  34056  cdleme32f  34058  ltrniotaval  34193  cdlemksv2  34459  cdlemkuv2  34479  cdlemk36  34525  cdlemk38  34527  cdlemk19x  34555  cdlemk11t  34558  mzpsubst  35635  aomclem8  35964  binomcxplemdvbinom  36746  binomcxplemdvsum  36748  binomcxplemnotnn0  36749  evth2f  37376  fvelrnbf  37379  evthf  37388  rfcnpre3  37394  rfcnpre4  37395  rfcnnnub  37397  refsum2cnlem1  37398  dffo3f  37488  fmul01  37696  fmuldfeqlem1  37698  fmuldfeq  37699  fmul01lt1lem1  37700  fmul01lt1lem2  37701  fmul01lt1  37702  cncfmptss  37703  mulc1cncfg  37705  expcnfg  37709  fprodabs2  37713  climmulf  37720  climexp  37721  climsuse  37725  climrecf  37726  climinff  37728  climinffOLD  37729  climaddf  37733  mullimc  37734  idlimc  37744  limcperiod  37746  neglimc  37766  addlimc  37767  0ellimcdiv  37768  cncfshift  37789  icccncfext  37803  cncficcgt0  37804  cncfiooicclem1  37809  dvnmul  37856  dvnprodlem1  37859  itgsubsticclem  37890  stoweidlem3  37901  stoweidlem23  37921  stoweidlem26  37924  stoweidlem28  37926  stoweidlem29  37927  stoweidlem29OLD  37928  stoweidlem31  37930  stoweidlem34  37933  stoweidlem36  37935  stoweidlem42  37941  stoweidlem48  37947  stoweidlem51  37950  stoweidlem52  37951  stoweidlem59  37958  wallispilem5  37969  stirlinglem4  37977  stirlinglem11  37984  stirlinglem12  37985  stirlinglem13  37986  stirlinglem14  37987  stirlinglem15  37988  fourierdlem20  38027  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem79  38087  fourierdlem89  38097  fourierdlem91  38099  fourierdlem112  38120  fourierdlem115  38123  fourierd  38124  fourierclimd  38125  etransclem2  38139  etransclem48OLD  38185  etransclem48  38186  sge0revalmpt  38258  sge0fsummpt  38270  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0iunmpt  38298  sge0xadd  38315  sge0fsummptf  38316  sge0gtfsumgt  38323  iundjiun  38336  meadjiun  38342  omeiunle  38376  omeiunltfirp  38378  ovncvrrp  38424  nfafv  38676
  Copyright terms: Public domain W3C validator