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

Theorem fvmpt2 5812
Description: Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
Hypothesis
Ref Expression
fvmpt2.1  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
fvmpt2  |-  ( ( x  e.  A  /\  B  e.  C )  ->  ( F `  x
)  =  B )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)    F( x)

Proof of Theorem fvmpt2
StepHypRef Expression
1 fvmpt2.1 . . 3  |-  F  =  ( x  e.  A  |->  B )
21fvmpt2i 5811 . 2  |-  ( x  e.  A  ->  ( F `  x )  =  (  _I  `  B
) )
3 fvi 5783 . 2  |-  ( B  e.  C  ->  (  _I  `  B )  =  B )
42, 3sylan9eq 2488 1  |-  ( ( x  e.  A  /\  B  e.  C )  ->  ( F `  x
)  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725    e. cmpt 4266    _I cid 4493   ` cfv 5454
This theorem is referenced by:  fvmptss  5813  fvmpt2d  5814  fvmptdf  5816  mpteqb  5819  fvmptt  5820  fvmptf  5821  ralrnmpt  5878  fmptco  5901  f1mpt  6007  offval2  6322  ofrfval2  6323  mptelixpg  7099  dom2lem  7147  mapxpen  7273  xpmapenlem  7274  cnfcom3clem  7662  tcvalg  7677  rankf  7720  infxpenc2lem2  7901  dfac8clem  7913  acni2  7927  acnlem  7929  fin23lem32  8224  axcc2lem  8316  axcc3  8318  domtriomlem  8322  ac6num  8359  konigthlem  8443  rpnnen1lem1  10600  rpnnen1lem3  10602  rpnnen1lem5  10604  seqof  11380  seqof2  11381  rlim2  12290  ello1mpt  12315  o1compt  12381  sumrblem  12505  fsumcvg  12506  summolem2a  12509  zsum  12512  fsum  12514  fsumcvg2  12521  fsumadd  12532  isummulc2  12546  fsummulc2  12567  fsumrelem  12586  iserodd  13209  prmrec  13290  prdsbas3  13703  prdsdsval2  13706  invfuc  14171  yonedalem4c  14374  gsumconst  15532  prdsgsum  15552  dprdwd  15569  gsumdixp  15715  evlslem4  16564  elptr2  17606  ptunimpt  17627  ptcldmpt  17646  ptclsg  17647  txcnp  17652  ptcnplem  17653  cnmpt11  17695  cnmpt1t  17697  cnmptk2  17718  xkocnv  17846  flfcnp2  18039  ustn0  18250  utopsnneiplem  18277  ucnima  18311  iccpnfcnv  18969  ovolctb  19386  ovoliunlem1  19398  ovoliun2  19402  ovolshftlem1  19405  ovolscalem1  19409  voliun  19448  ioombl1lem3  19454  ioombl1lem4  19455  uniioombllem2  19475  mbfeqalem  19534  mbfpos  19543  mbfposr  19544  mbfposb  19545  mbfsup  19556  mbfinf  19557  mbflim  19560  i1fposd  19599  itg1climres  19606  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1fseqlem6  19612  itg2split  19641  itg2mono  19645  itg2cnlem1  19653  isibl2  19658  itgmpt  19674  itgeqa  19705  itggt0  19733  itgcn  19734  limcmpt  19770  dvlipcn  19878  lhop2  19899  dvfsumabs  19907  itgparts  19931  itgsubstlem  19932  itgsubst  19933  elplyd  20121  coeeulem  20143  coeeq2  20161  dvply1  20201  plyremlem  20221  ulmss  20313  ulmdvlem1  20316  mtest  20320  itgulm2  20325  radcnvlem1  20329  pserulm  20338  leibpi  20782  rlimcnp  20804  o1cxp  20813  sqff1o  20965  lgseisenlem2  21134  dchrvmasumlem1  21189  ubthlem1  22372  cnlnadjlem5  23574  xppreima2  24060  abfmpunirn  24064  xrmulc1cn  24316  esumpcvgval  24468  voliune  24585  lgamgulmlem2  24814  lgamgulmlem6  24818  lgamgulm2  24820  iscvm  24946  prodrblem  25255  fprodcvg  25256  prodmolem2a  25260  zprod  25263  fprod  25267  fprodmul  25284  fproddiv  25285  itg2addnclem  26256  itggt0cn  26277  ftc1anclem5  26284  elrfirn2  26750  eq0rabdioph  26835  monotoddzz  27006  aomclem2  27130  refsumcn  27677  refsum2cnlem1  27684  fmuldfeqlem1  27688  fmuldfeq  27689  climneg  27712  climdivf  27714  itgsin0pilem1  27720  ibliccsinexp  27721  itgsinexplem1  27724  itgsinexp  27725  stoweidlem2  27727  stoweidlem11  27736  stoweidlem12  27737  stoweidlem16  27741  stoweidlem17  27742  stoweidlem18  27743  stoweidlem19  27744  stoweidlem20  27745  stoweidlem21  27746  stoweidlem22  27747  stoweidlem23  27748  stoweidlem27  27752  stoweidlem31  27756  stoweidlem34  27759  stoweidlem36  27761  stoweidlem40  27765  stoweidlem41  27766  stoweidlem42  27767  stoweidlem48  27773  stoweidlem55  27780  stoweidlem59  27784  stoweidlem62  27787  stirlinglem3  27801  stirlinglem8  27806  stirlinglem14  27812  stirlinglem15  27813  stirlingr  27815  frgrancvvdeqlem6  28424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fv 5462
  Copyright terms: Public domain W3C validator