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

Theorem nffvmpt1 5872
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 4536 . 2  |-  F/_ x
( x  e.  A  |->  B )
2 nfcv 2629 . 2  |-  F/_ x C
31, 2nffv 5871 1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2615    |-> cmpt 4505   ` cfv 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-iota 5549  df-fv 5594
This theorem is referenced by:  fvmptt  5963  fmptco  6052  offval2  6538  ofrfval2  6539  mptelixpg  7503  dom2lem  7552  cantnflem1  8104  acni2  8423  axcc2  8813  seqof2  12129  rlim2  13278  ello1mpt  13303  o1compt  13369  sumfc  13490  fsum  13501  fsumf1o  13504  sumss  13505  fsumcvg2  13508  fsumadd  13520  isummulc2  13536  fsummulc2  13558  fsumrelem  13580  isumshft  13610  iserodd  14214  prdsbas3  14732  prdsdsval2  14735  invfuc  15197  yonedalem4b  15399  dprdwd  16835  dprdwdOLD  16841  gsumdixpOLD  17041  gsumdixp  17042  evlslem4OLD  17944  evlslem4  17945  elptr2  19810  ptunimpt  19831  ptcldmpt  19850  ptclsg  19851  txcnp  19856  ptcnplem  19857  cnmpt1t  19901  cnmptk2  19922  flfcnp2  20243  voliun  21699  mbfeqalem  21784  mbfpos  21793  mbfposb  21795  mbfsup  21806  mbfinf  21807  mbflim  21810  i1fposd  21849  isibl2  21908  itgmpt  21924  itgeqa  21955  itggt0  21983  itgcn  21984  limcmpt  22022  lhop2  22151  itgsubstlem  22184  itgsubst  22185  elplyd  22334  coeeq2  22374  dgrle  22375  ulmss  22526  itgulm2  22538  leibpi  23001  rlimcnp  23023  o1cxp  23032  fmptcof2  27174  offval2f  27178  lgamgulmlem2  28212  lgamgulmlem6  28216  zprod  28646  fprod  28650  prodfc  28654  fprodf1o  28655  fprodmul  28667  fproddiv  28668  itggt0cn  29664  elrfirn2  30232  eq0rabdioph  30314  monotoddzz  30483  aomclem8  30611  fmuldfeq  31133
  Copyright terms: Public domain W3C validator