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

Theorem nffvmpt1 5861
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 4523 . 2  |-  F/_ x
( x  e.  A  |->  B )
2 nfcv 2603 . 2  |-  F/_ x C
31, 2nffv 5860 1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2589    |-> cmpt 4492   ` cfv 5575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-iota 5538  df-fv 5583
This theorem is referenced by:  fvmptt  5953  fmptco  6046  offval2  6538  ofrfval2  6539  mptelixpg  7505  dom2lem  7554  cantnflem1  8108  acni2  8427  axcc2  8817  seqof2  12141  rlim2  13295  ello1mpt  13320  o1compt  13386  sumfc  13507  fsum  13518  fsumf1o  13521  sumss  13522  fsumcvg2  13525  fsumadd  13537  isummulc2  13553  fsummulc2  13575  fsumrelem  13597  isumshft  13627  iserodd  14233  prdsbas3  14752  prdsdsval2  14755  invfuc  15214  yonedalem4b  15416  dprdwdOLD2  16916  dprdwdOLD  16922  gsumdixpOLD  17128  gsumdixp  17129  evlslem4OLD  18044  evlslem4  18045  elptr2  19945  ptunimpt  19966  ptcldmpt  19985  ptclsg  19986  txcnp  19991  ptcnplem  19992  cnmpt1t  20036  cnmptk2  20057  flfcnp2  20378  voliun  21834  mbfeqalem  21919  mbfpos  21928  mbfposb  21930  mbfsup  21941  mbfinf  21942  mbflim  21945  i1fposd  21984  isibl2  22043  itgmpt  22059  itgeqa  22090  itggt0  22118  itgcn  22119  limcmpt  22157  lhop2  22286  itgsubstlem  22319  itgsubst  22320  elplyd  22469  coeeq2  22509  dgrle  22510  ulmss  22661  itgulm2  22673  leibpi  23142  rlimcnp  23164  o1cxp  23173  fmptcof2  27371  offval2f  27375  lgamgulmlem2  28442  lgamgulmlem6  28446  zprod  29041  fprod  29045  prodfc  29049  fprodf1o  29050  fprodmul  29062  fproddiv  29063  itggt0cn  30059  elrfirn2  30600  eq0rabdioph  30682  monotoddzz  30851  aomclem8  30979  fmuldfeq  31505
  Copyright terms: Public domain W3C validator