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

Theorem nffvmpt1 5687
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 4369 . 2  |-  F/_ x
( x  e.  A  |->  B )
2 nfcv 2569 . 2  |-  F/_ x C
31, 2nffv 5686 1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2556    e. cmpt 4338   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-iota 5369  df-fv 5414
This theorem is referenced by:  fvmptt  5777  fmptco  5863  offval2  6325  ofrfval2  6326  mptelixpg  7288  dom2lem  7337  cantnflem1  7885  acni2  8204  axcc2  8594  seqof2  11847  rlim2  12957  ello1mpt  12982  o1compt  13048  sumfc  13169  fsum  13180  fsumf1o  13183  sumss  13184  fsumcvg2  13187  fsumadd  13198  isummulc2  13212  fsummulc2  13233  fsumrelem  13252  isumshft  13284  iserodd  13884  prdsbas3  14401  prdsdsval2  14404  invfuc  14866  yonedalem4b  15068  dprdwd  16468  dprdwdOLD  16474  gsumdixpOLD  16634  gsumdixp  16635  evlslem4OLD  17517  evlslem4  17518  elptr2  18988  ptunimpt  19009  ptcldmpt  19028  ptclsg  19029  txcnp  19034  ptcnplem  19035  cnmpt1t  19079  cnmptk2  19100  flfcnp2  19421  voliun  20876  mbfeqalem  20961  mbfpos  20970  mbfposb  20972  mbfsup  20983  mbfinf  20984  mbflim  20987  i1fposd  21026  isibl2  21085  itgmpt  21101  itgeqa  21132  itggt0  21160  itgcn  21161  limcmpt  21199  lhop2  21328  itgsubstlem  21361  itgsubst  21362  elplyd  21554  coeeq2  21594  dgrle  21595  ulmss  21746  itgulm2  21758  leibpi  22221  rlimcnp  22243  o1cxp  22252  fmptcof2  25802  offval2f  25806  lgamgulmlem2  26863  lgamgulmlem6  26867  zprod  27296  fprod  27300  prodfc  27304  fprodf1o  27305  fprodmul  27317  fproddiv  27318  itggt0cn  28305  elrfirn2  28874  eq0rabdioph  28957  monotoddzz  29126  aomclem8  29256  fmuldfeq  29606
  Copyright terms: Public domain W3C validator