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

Theorem nffvmpt1 5765
Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
Assertion
Ref Expression
nffvmpt1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Distinct variable group:    x, C
Allowed substitution hints:    A( x)    B( x)

Proof of Theorem nffvmpt1
StepHypRef Expression
1 nfmpt1 4323 . 2  |-  F/_ x
( x  e.  A  |->  B )
2 nfcv 2578 . 2  |-  F/_ x C
31, 2nffv 5764 1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2565    e. cmpt 4291   ` cfv 5483
This theorem is referenced by:  fvmptt  5849  fmptco  5930  offval2  6351  ofrfval2  6352  mptelixpg  7128  dom2lem  7176  acni2  7958  axcc2  8348  seqof2  11412  rlim2  12321  ello1mpt  12346  o1compt  12412  sumfc  12534  zsum  12543  fsum  12545  fsumf1o  12548  sumss  12549  fsumcvg2  12552  fsumadd  12563  isummulc2  12577  fsummulc2  12598  fsumrelem  12617  isumshft  12650  iserodd  13240  prdsbas3  13734  prdsdsval2  13737  invfuc  14202  yonedalem4b  14404  dprdwd  15600  gsumdixp  15746  evlslem4  16595  elptr2  17637  ptunimpt  17658  ptcldmpt  17677  ptclsg  17678  txcnp  17683  ptcnplem  17684  cnmpt1t  17728  cnmptk2  17749  flfcnp2  18070  voliun  19479  mbfeqalem  19563  mbfpos  19572  mbfposb  19574  mbfsup  19585  mbfinf  19586  mbflim  19589  i1fposd  19628  isibl2  19687  itgmpt  19703  itgeqa  19734  itggt0  19762  itgcn  19763  limcmpt  19801  lhop2  19930  itgsubstlem  19963  itgsubst  19964  elplyd  20152  coeeq2  20192  dgrle  20193  ulmss  20344  itgulm2  20356  leibpi  20813  rlimcnp  20835  o1cxp  20844  fmptcof2  24107  offval2f  24111  lgamgulmlem2  24845  lgamgulmlem6  24849  zprod  25294  fprod  25298  prodfc  25302  fprodf1o  25303  fprodmul  25315  fproddiv  25316  itggt0cn  26315  elrfirn2  26788  eq0rabdioph  26873  monotoddzz  27044  aomclem8  27174  fmuldfeq  27727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-iota 5447  df-fv 5491
  Copyright terms: Public domain W3C validator