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

Theorem nffvmpt1 5703
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 4266 . 2  |-  F/_ x
( x  e.  A  |->  B )
2 nfcv 2548 . 2  |-  F/_ x C
31, 2nffv 5702 1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2535    e. cmpt 4234   ` cfv 5421
This theorem is referenced by:  fvmptt  5787  fmptco  5868  offval2  6289  ofrfval2  6290  mptelixpg  7066  dom2lem  7114  acni2  7891  axcc2  8281  seqof2  11344  rlim2  12253  ello1mpt  12278  o1compt  12344  sumfc  12466  zsum  12475  fsum  12477  fsumf1o  12480  sumss  12481  fsumcvg2  12484  fsumadd  12495  isummulc2  12509  fsummulc2  12530  fsumrelem  12549  isumshft  12582  iserodd  13172  prdsbas3  13666  prdsdsval2  13669  invfuc  14134  yonedalem4b  14336  dprdwd  15532  gsumdixp  15678  evlslem4  16527  elptr2  17567  ptunimpt  17588  ptcldmpt  17607  ptclsg  17608  txcnp  17613  ptcnplem  17614  cnmpt1t  17658  cnmptk2  17679  flfcnp2  18000  voliun  19409  mbfeqalem  19495  mbfpos  19504  mbfposb  19506  mbfsup  19517  mbfinf  19518  mbflim  19521  i1fposd  19560  isibl2  19619  itgmpt  19635  itgeqa  19666  itggt0  19694  itgcn  19695  limcmpt  19731  lhop2  19860  itgsubstlem  19893  itgsubst  19894  elplyd  20082  coeeq2  20122  dgrle  20123  ulmss  20274  itgulm2  20286  leibpi  20743  rlimcnp  20765  o1cxp  20774  fmptcof2  24037  offval2f  24041  lgamgulmlem2  24775  lgamgulmlem6  24779  zprod  25224  fprod  25228  prodfc  25232  fprodf1o  25233  fprodmul  25245  fproddiv  25246  itggt0cn  26184  elrfirn2  26648  eq0rabdioph  26733  monotoddzz  26904  aomclem8  27035  fmuldfeq  27588
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-iota 5385  df-fv 5429
  Copyright terms: Public domain W3C validator