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

Theorem nffv 5726
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 5453 . 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 5413 . 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 5407   ` cfv 5445
This theorem is referenced by:  nffvmpt1  5727  nffvd  5728  dffn5f  5772  fvmptss  5804  fvmptex  5806  fvmptf  5812  fvmptnf  5813  eqfnfv2f  5822  ralrnmpt  5869  ffnfvf  5886  funiunfvf  5987  dff13f  5997  nfiso  6035  nfriota1  6548  nfrecs  6626  nfrdg  6663  rdgsucmptf  6677  rdgsucmptnf  6678  frsucmpt  6686  frsucmptn  6687  rankidb  7715  rankval4  7782  dfac8clem  7902  cardaleph  7959  hsmexlem2  8296  axcc2  8306  uniimadomf  8409  nfseq  11321  seqof2  11369  rlim2  12278  nfsum1  12472  nfsum  12473  fsumrelem  12574  o1fsum  12580  prdsbas3  13691  prdsdsval2  13694  yonedalem4b  14361  gsum2d2lem  15535  ptcldmpt  17634  ptcnp  17642  cnmpt11  17683  cnmpt21  17691  cnmptk2  17706  prdsdsf  18385  prdsxmet  18387  ovolfiniun  19385  ovoliunlem3  19388  ovoliun  19389  ovoliun2  19390  ovoliunnul  19391  volfiniun  19429  voliun  19436  mbfsup  19544  mbflim  19548  itg2splitlem  19628  itg2split  19629  itg2cnlem1  19641  isibl2  19646  nfitg1  19653  nfitg  19654  cbvitg  19655  itgabs  19714  dvlipcn  19866  lhop2  19887  dvfsumabs  19895  dvfsumrlim  19903  itgparts  19919  itgsubstlem  19920  ulmss  20301  itgulm2  20313  lgseisenlem2  21122  dchrisumlem3  21173  cnlnadjlem5  23562  dfimafnf  24031  esumfzf  24447  voliune  24573  volfiniune  24574  lgamgulmlem2  24802  lgamgulmlem6  24806  lgamgulm2  24808  cvmcov  24938  nfcprod1  25225  nfcprod  25226  fprodefsum  25287  trpredlem1  25485  trpredrec  25496  sltval2  25565  nobndlem5  25605  itgabsnc  26220  ftc1cnnclem  26224  mzpsubst  26742  aomclem8  27074  evth2f  27600  fvelrnbf  27603  evthf  27612  rfcnpre3  27618  rfcnpre4  27619  rfcnnnub  27621  refsum2cnlem1  27622  fmul01  27624  fmuldfeqlem1  27626  fmuldfeq  27627  fmul01lt1lem1  27628  fmul01lt1lem2  27629  fmul01lt1  27630  cncfmptss  27631  mulc1cncfg  27635  expcnfg  27640  climmulf  27644  climexp  27645  climsuse  27648  climrecf  27649  climinff  27651  stoweidlem3  27666  stoweidlem23  27686  stoweidlem26  27689  stoweidlem28  27691  stoweidlem29  27692  stoweidlem31  27694  stoweidlem34  27697  stoweidlem36  27699  stoweidlem42  27705  stoweidlem48  27711  stoweidlem51  27714  stoweidlem52  27715  stoweidlem59  27722  wallispilem5  27732  stirlinglem4  27740  stirlinglem11  27747  stirlinglem12  27748  stirlinglem13  27749  stirlinglem14  27750  stirlinglem15  27751  nfafv  27914  bnj1534  29078  bnj1542  29082  bnj958  29165  bnj1000  29166  bnj1446  29268  bnj1447  29269  bnj1448  29270  bnj1466  29276  bnj1467  29277  bnj1519  29288  bnj1520  29289  bnj1529  29293  riotaocN  29846  cdleme32d  31080  cdleme32f  31082  ltrniotaval  31217  cdlemksv2  31483  cdlemkuv2  31503  cdlemk36  31549  cdlemk38  31551  cdlemk19x  31579  cdlemk11t  31582
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 5409  df-fv 5453
  Copyright terms: Public domain W3C validator