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

Theorem nffv 5693
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 5421 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2574 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4331 . . 3  |-  F/ x  A F y
65nfiota 5380 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2571 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2561   class class class wbr 4287   iotacio 5374   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421
This theorem is referenced by:  nffvmpt1  5694  nffvd  5695  dffn5f  5741  fvmptss  5777  fvmptex  5779  fvmptf  5785  fvmptnf  5786  eqfnfv2f  5796  ralrnmpt  5847  ffnfvf  5865  funiunfvf  5961  dff13f  5968  nfiso  6010  nfrecs  6826  nfrdg  6862  rdgsucmptf  6876  rdgsucmptnf  6877  frsucmpt  6885  frsucmptn  6886  rankidb  7999  rankval4  8066  dfac8clem  8194  cardaleph  8251  hsmexlem2  8588  axcc2  8598  uniimadomf  8701  nfseq  11808  seqof2  11856  rlim2  12966  nfsum1  13159  nfsum  13160  sumeq2ii  13162  fsumrelem  13262  o1fsum  13268  prdsbas3  14411  prdsdsval2  14414  yonedalem4b  15078  gsum2d2lem  16453  evl1gsumdlem  17765  ptcldmpt  19162  ptcnp  19170  cnmpt11  19211  cnmpt21  19219  cnmptk2  19234  prdsdsf  19917  prdsxmet  19919  ovolfiniun  20959  ovoliunlem3  20962  ovoliun  20963  ovoliun2  20964  ovoliunnul  20965  volfiniun  21003  voliun  21010  mbfsup  21117  mbflim  21121  itg2splitlem  21201  itg2split  21202  itg2cnlem1  21214  isibl2  21219  nfitg1  21226  nfitg  21227  cbvitg  21228  itgabs  21287  dvlipcn  21441  lhop2  21462  dvfsumabs  21470  dvfsumrlim  21478  itgparts  21494  itgsubstlem  21495  ulmss  21837  itgulm2  21849  lgseisenlem2  22664  dchrisumlem3  22715  cnlnadjlem5  25426  dfimafnf  25901  esumfzf  26470  voliune  26597  volfiniune  26598  lgamgulmlem2  26968  lgamgulmlem6  26972  lgamgulm2  26974  cvmcov  27104  nfcprod1  27374  nfcprod  27375  fprodefsum  27436  trpredlem1  27642  trpredrec  27653  nfwrecs  27670  sltval2  27748  nobndlem5  27788  itgabsnc  28414  mzpsubst  29038  aomclem8  29367  evth2f  29690  fvelrnbf  29693  evthf  29702  rfcnpre3  29708  rfcnpre4  29709  rfcnnnub  29711  refsum2cnlem1  29712  fmul01  29714  fmuldfeqlem1  29716  fmuldfeq  29717  fmul01lt1lem1  29718  fmul01lt1lem2  29719  fmul01lt1  29720  cncfmptss  29721  mulc1cncfg  29723  expcnfg  29726  climmulf  29730  climexp  29731  climsuse  29734  climrecf  29735  climinff  29737  stoweidlem3  29751  stoweidlem23  29771  stoweidlem26  29774  stoweidlem28  29776  stoweidlem29  29777  stoweidlem31  29779  stoweidlem34  29782  stoweidlem36  29784  stoweidlem42  29790  stoweidlem48  29796  stoweidlem51  29799  stoweidlem52  29800  stoweidlem59  29807  wallispilem5  29817  stirlinglem4  29825  stirlinglem11  29832  stirlinglem12  29833  stirlinglem13  29834  stirlinglem14  29835  stirlinglem15  29836  nfafv  29995  bnj1534  31733  bnj1542  31737  bnj958  31820  bnj1000  31821  bnj1446  31923  bnj1447  31924  bnj1448  31925  bnj1466  31931  bnj1467  31932  bnj1519  31943  bnj1520  31944  bnj1529  31948  riotaocN  32694  cdleme32d  33928  cdleme32f  33930  ltrniotaval  34065  cdlemksv2  34331  cdlemkuv2  34351  cdlemk36  34397  cdlemk38  34399  cdlemk19x  34427  cdlemk11t  34430
  Copyright terms: Public domain W3C validator