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

Theorem nffvmpt1 5704
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 4386 . 2  |-  F/_ x
( x  e.  A  |->  B )
2 nfcv 2584 . 2  |-  F/_ x C
31, 2nffv 5703 1  |-  F/_ x
( ( x  e.  A  |->  B ) `  C )
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2571    e. cmpt 4355   ` cfv 5423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-iota 5386  df-fv 5431
This theorem is referenced by:  fvmptt  5794  fmptco  5881  offval2  6341  ofrfval2  6342  mptelixpg  7305  dom2lem  7354  cantnflem1  7902  acni2  8221  axcc2  8611  seqof2  11869  rlim2  12979  ello1mpt  13004  o1compt  13070  sumfc  13191  fsum  13202  fsumf1o  13205  sumss  13206  fsumcvg2  13209  fsumadd  13220  isummulc2  13234  fsummulc2  13256  fsumrelem  13275  isumshft  13307  iserodd  13907  prdsbas3  14424  prdsdsval2  14427  invfuc  14889  yonedalem4b  15091  dprdwd  16500  dprdwdOLD  16506  gsumdixpOLD  16705  gsumdixp  16706  evlslem4OLD  17595  evlslem4  17596  elptr2  19152  ptunimpt  19173  ptcldmpt  19192  ptclsg  19193  txcnp  19198  ptcnplem  19199  cnmpt1t  19243  cnmptk2  19264  flfcnp2  19585  voliun  21040  mbfeqalem  21125  mbfpos  21134  mbfposb  21136  mbfsup  21147  mbfinf  21148  mbflim  21151  i1fposd  21190  isibl2  21249  itgmpt  21265  itgeqa  21296  itggt0  21324  itgcn  21325  limcmpt  21363  lhop2  21492  itgsubstlem  21525  itgsubst  21526  elplyd  21675  coeeq2  21715  dgrle  21716  ulmss  21867  itgulm2  21879  leibpi  22342  rlimcnp  22364  o1cxp  22373  fmptcof2  25984  offval2f  25988  lgamgulmlem2  27021  lgamgulmlem6  27025  zprod  27455  fprod  27459  prodfc  27463  fprodf1o  27464  fprodmul  27476  fproddiv  27477  itggt0cn  28469  elrfirn2  29037  eq0rabdioph  29120  monotoddzz  29289  aomclem8  29419  fmuldfeq  29769
  Copyright terms: Public domain W3C validator