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

Theorem nffv 5727
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 5454 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2571 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4248 . . 3  |-  F/ x  A F y
65nfiota 5414 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2568 1  |-  F/_ x
( F `  A
)
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2558   class class class wbr 4204   iotacio 5408   ` cfv 5446
This theorem is referenced by:  nffvmpt1  5728  nffvd  5729  dffn5f  5773  fvmptss  5805  fvmptex  5807  fvmptf  5813  fvmptnf  5814  eqfnfv2f  5823  ralrnmpt  5870  ffnfvf  5887  funiunfvf  5988  dff13f  5998  nfiso  6036  nfriota1  6549  nfrecs  6627  nfrdg  6664  rdgsucmptf  6678  rdgsucmptnf  6679  frsucmpt  6687  frsucmptn  6688  rankidb  7718  rankval4  7785  dfac8clem  7905  cardaleph  7962  hsmexlem2  8299  axcc2  8309  uniimadomf  8412  nfseq  11325  seqof2  11373  rlim2  12282  nfsum1  12476  nfsum  12477  fsumrelem  12578  o1fsum  12584  prdsbas3  13695  prdsdsval2  13698  yonedalem4b  14365  gsum2d2lem  15539  ptcldmpt  17638  ptcnp  17646  cnmpt11  17687  cnmpt21  17695  cnmptk2  17710  prdsdsf  18389  prdsxmet  18391  ovolfiniun  19389  ovoliunlem3  19392  ovoliun  19393  ovoliun2  19394  ovoliunnul  19395  volfiniun  19433  voliun  19440  mbfsup  19548  mbflim  19552  itg2splitlem  19632  itg2split  19633  itg2cnlem1  19645  isibl2  19650  nfitg1  19657  nfitg  19658  cbvitg  19659  itgabs  19718  dvlipcn  19870  lhop2  19891  dvfsumabs  19899  dvfsumrlim  19907  itgparts  19923  itgsubstlem  19924  ulmss  20305  itgulm2  20317  lgseisenlem2  21126  dchrisumlem3  21177  cnlnadjlem5  23566  dfimafnf  24035  esumfzf  24451  voliune  24577  volfiniune  24578  lgamgulmlem2  24806  lgamgulmlem6  24810  lgamgulm2  24812  cvmcov  24942  nfcprod1  25228  nfcprod  25229  fprodefsum  25290  trpredlem1  25497  trpredrec  25508  nfwrecs  25525  sltval2  25603  nobndlem5  25643  itgabsnc  26264  mzpsubst  26796  aomclem8  27127  evth2f  27653  fvelrnbf  27656  evthf  27665  rfcnpre3  27671  rfcnpre4  27672  rfcnnnub  27674  refsum2cnlem1  27675  fmul01  27677  fmuldfeqlem1  27679  fmuldfeq  27680  fmul01lt1lem1  27681  fmul01lt1lem2  27682  fmul01lt1  27683  cncfmptss  27684  mulc1cncfg  27688  expcnfg  27693  climmulf  27697  climexp  27698  climsuse  27701  climrecf  27702  climinff  27704  stoweidlem3  27719  stoweidlem23  27739  stoweidlem26  27742  stoweidlem28  27744  stoweidlem29  27745  stoweidlem31  27747  stoweidlem34  27750  stoweidlem36  27752  stoweidlem42  27758  stoweidlem48  27764  stoweidlem51  27767  stoweidlem52  27768  stoweidlem59  27775  wallispilem5  27785  stirlinglem4  27793  stirlinglem11  27800  stirlinglem12  27801  stirlinglem13  27802  stirlinglem14  27803  stirlinglem15  27804  nfafv  27967  bnj1534  29161  bnj1542  29165  bnj958  29248  bnj1000  29249  bnj1446  29351  bnj1447  29352  bnj1448  29353  bnj1466  29359  bnj1467  29360  bnj1519  29371  bnj1520  29372  bnj1529  29376  riotaocN  29944  cdleme32d  31178  cdleme32f  31180  ltrniotaval  31315  cdlemksv2  31581  cdlemkuv2  31601  cdlemk36  31647  cdlemk38  31649  cdlemk19x  31677  cdlemk11t  31680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454
  Copyright terms: Public domain W3C validator