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

Theorem nffv 5805
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 5533 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2616 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4443 . . 3  |-  F/ x  A F y
65nfiota 5492 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2614 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2602   class class class wbr 4399   iotacio 5486   ` cfv 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533
This theorem is referenced by:  nffvmpt1  5806  nffvd  5807  dffn5f  5854  fvmptss  5890  fvmptex  5892  fvmptf  5898  fvmptnf  5899  eqfnfv2f  5909  ralrnmpt  5960  ffnfvf  5978  funiunfvf  6074  dff13f  6081  nfiso  6123  nfrecs  6943  nfrdg  6979  rdgsucmptf  6993  rdgsucmptnf  6994  frsucmpt  7002  frsucmptn  7003  rankidb  8117  rankval4  8184  dfac8clem  8312  cardaleph  8369  hsmexlem2  8706  axcc2  8716  uniimadomf  8819  nfseq  11932  seqof2  11980  rlim2  13091  nfsum1  13284  nfsum  13285  sumeq2ii  13287  fsumrelem  13387  o1fsum  13393  prdsbas3  14537  prdsdsval2  14540  yonedalem4b  15204  gsum2d2lem  16586  evl1gsumdlem  17914  ptcldmpt  19318  ptcnp  19326  cnmpt11  19367  cnmpt21  19375  cnmptk2  19390  prdsdsf  20073  prdsxmet  20075  ovolfiniun  21115  ovoliunlem3  21118  ovoliun  21119  ovoliun2  21120  ovoliunnul  21121  volfiniun  21160  voliun  21167  mbfsup  21274  mbflim  21278  itg2splitlem  21358  itg2split  21359  itg2cnlem1  21371  isibl2  21376  nfitg1  21383  nfitg  21384  cbvitg  21385  itgabs  21444  dvlipcn  21598  lhop2  21619  dvfsumabs  21627  dvfsumrlim  21635  itgparts  21651  itgsubstlem  21652  ulmss  21994  itgulm2  22006  lgseisenlem2  22821  dchrisumlem3  22872  cnlnadjlem5  25626  dfimafnf  26100  esumfzf  26662  voliune  26788  volfiniune  26789  lgamgulmlem2  27159  lgamgulmlem6  27163  lgamgulm2  27165  cvmcov  27295  nfcprod1  27566  nfcprod  27567  fprodefsum  27628  trpredlem1  27834  trpredrec  27845  nfwrecs  27862  sltval2  27940  nobndlem5  27980  itgabsnc  28608  mzpsubst  29232  aomclem8  29561  evth2f  29884  fvelrnbf  29887  evthf  29896  rfcnpre3  29902  rfcnpre4  29903  rfcnnnub  29905  refsum2cnlem1  29906  fmul01  29908  fmuldfeqlem1  29910  fmuldfeq  29911  fmul01lt1lem1  29912  fmul01lt1lem2  29913  fmul01lt1  29914  cncfmptss  29915  mulc1cncfg  29917  expcnfg  29920  climmulf  29924  climexp  29925  climsuse  29928  climrecf  29929  climinff  29931  stoweidlem3  29945  stoweidlem23  29965  stoweidlem26  29968  stoweidlem28  29970  stoweidlem29  29971  stoweidlem31  29973  stoweidlem34  29976  stoweidlem36  29978  stoweidlem42  29984  stoweidlem48  29990  stoweidlem51  29993  stoweidlem52  29994  stoweidlem59  30001  wallispilem5  30011  stirlinglem4  30019  stirlinglem11  30026  stirlinglem12  30027  stirlinglem13  30028  stirlinglem14  30029  stirlinglem15  30030  nfafv  30189  coe1fzgsumdlem  30989  bnj1534  32163  bnj1542  32167  bnj958  32250  bnj1000  32251  bnj1446  32353  bnj1447  32354  bnj1448  32355  bnj1466  32361  bnj1467  32362  bnj1519  32373  bnj1520  32374  bnj1529  32378  riotaocN  33177  cdleme32d  34411  cdleme32f  34413  ltrniotaval  34548  cdlemksv2  34814  cdlemkuv2  34834  cdlemk36  34880  cdlemk38  34882  cdlemk19x  34910  cdlemk11t  34913
  Copyright terms: Public domain W3C validator