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

Theorem nffv 5686
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 5414 . 2  |-  ( F `
 A )  =  ( iota y A F y )
2 nffv.2 . . . 4  |-  F/_ x A
3 nffv.1 . . . 4  |-  F/_ x F
4 nfcv 2569 . . . 4  |-  F/_ x
y
52, 3, 4nfbr 4324 . . 3  |-  F/ x  A F y
65nfiota 5373 . 2  |-  F/_ x
( iota y A F y )
71, 6nfcxfr 2566 1  |-  F/_ x
( F `  A
)
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2556   class class class wbr 4280   iotacio 5367   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414
This theorem is referenced by:  nffvmpt1  5687  nffvd  5688  dffn5f  5734  fvmptss  5770  fvmptex  5772  fvmptf  5778  fvmptnf  5779  eqfnfv2f  5789  ralrnmpt  5840  ffnfvf  5857  funiunfvf  5953  dff13f  5960  nfiso  6002  nfrecs  6820  nfrdg  6856  rdgsucmptf  6870  rdgsucmptnf  6871  frsucmpt  6879  frsucmptn  6880  rankidb  7995  rankval4  8062  dfac8clem  8190  cardaleph  8247  hsmexlem2  8584  axcc2  8594  uniimadomf  8697  nfseq  11800  seqof2  11848  rlim2  12958  nfsum1  13151  nfsum  13152  sumeq2ii  13154  fsumrelem  13253  o1fsum  13259  prdsbas3  14402  prdsdsval2  14405  yonedalem4b  15069  gsum2d2lem  16439  ptcldmpt  19029  ptcnp  19037  cnmpt11  19078  cnmpt21  19086  cnmptk2  19101  prdsdsf  19784  prdsxmet  19786  ovolfiniun  20826  ovoliunlem3  20829  ovoliun  20830  ovoliun2  20831  ovoliunnul  20832  volfiniun  20870  voliun  20877  mbfsup  20984  mbflim  20988  itg2splitlem  21068  itg2split  21069  itg2cnlem1  21081  isibl2  21086  nfitg1  21093  nfitg  21094  cbvitg  21095  itgabs  21154  dvlipcn  21308  lhop2  21329  dvfsumabs  21337  dvfsumrlim  21345  itgparts  21361  itgsubstlem  21362  ulmss  21747  itgulm2  21759  lgseisenlem2  22574  dchrisumlem3  22625  cnlnadjlem5  25298  dfimafnf  25774  esumfzf  26372  voliune  26499  volfiniune  26500  lgamgulmlem2  26864  lgamgulmlem6  26868  lgamgulm2  26870  cvmcov  27000  nfcprod1  27270  nfcprod  27271  fprodefsum  27332  trpredlem1  27538  trpredrec  27549  nfwrecs  27566  sltval2  27644  nobndlem5  27684  itgabsnc  28305  mzpsubst  28930  aomclem8  29259  evth2f  29582  fvelrnbf  29585  evthf  29594  rfcnpre3  29600  rfcnpre4  29601  rfcnnnub  29603  refsum2cnlem1  29604  fmul01  29606  fmuldfeqlem1  29608  fmuldfeq  29609  fmul01lt1lem1  29610  fmul01lt1lem2  29611  fmul01lt1  29612  cncfmptss  29613  mulc1cncfg  29616  expcnfg  29619  climmulf  29623  climexp  29624  climsuse  29627  climrecf  29628  climinff  29630  stoweidlem3  29644  stoweidlem23  29664  stoweidlem26  29667  stoweidlem28  29669  stoweidlem29  29670  stoweidlem31  29672  stoweidlem34  29675  stoweidlem36  29677  stoweidlem42  29683  stoweidlem48  29689  stoweidlem51  29692  stoweidlem52  29693  stoweidlem59  29700  wallispilem5  29710  stirlinglem4  29718  stirlinglem11  29725  stirlinglem12  29726  stirlinglem13  29727  stirlinglem14  29728  stirlinglem15  29729  nfafv  29888  bnj1534  31569  bnj1542  31573  bnj958  31656  bnj1000  31657  bnj1446  31759  bnj1447  31760  bnj1448  31761  bnj1466  31767  bnj1467  31768  bnj1519  31779  bnj1520  31780  bnj1529  31784  riotaocN  32448  cdleme32d  33682  cdleme32f  33684  ltrniotaval  33819  cdlemksv2  34085  cdlemkuv2  34105  cdlemk36  34151  cdlemk38  34153  cdlemk19x  34181  cdlemk11t  34184
  Copyright terms: Public domain W3C validator