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

Theorem fvmpt2 5460
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 5459 . 2  |-  ( x  e.  A  ->  ( F `  x )  =  (  _I  `  B
) )
3 fvi 5431 . 2  |-  ( B  e.  C  ->  (  _I  `  B )  =  B )
42, 3sylan9eq 2305 1  |-  ( ( x  e.  A  /\  B  e.  C )  ->  ( F `  x
)  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621    e. cmpt 3974    _I cid 4197   ` cfv 4592
This theorem is referenced by:  fvmptss  5461  fvmptdf  5463  mpteqb  5466  fvmptt  5467  fvmptf  5468  ralrnmpt  5521  fmptco  5543  f1mpt  5637  offval2  5947  ofrfval2  5948  mptelixpg  6739  dom2lem  6787  mapxpen  6912  xpmapenlem  6913  cnfcom3clem  7292  tcvalg  7307  rankf  7350  infxpenc2lem2  7531  dfac8clem  7543  acni2  7557  acnlem  7559  fin23lem32  7854  axcc2lem  7946  axcc3  7948  domtriomlem  7952  ac6num  7990  konigthlem  8070  rpnnen1lem1  10221  rpnnen1lem3  10223  rpnnen1lem5  10225  seqof  10981  rlim2  11847  ello1mpt  11872  o1compt  11938  sumrblem  12061  fsumcvg  12062  summolem2a  12065  zsum  12068  fsum  12070  fsumcvg2  12077  fsumadd  12088  isummulc2  12102  fsummulc2  12123  fsumrelem  12142  iserodd  12762  prmrec  12843  prdsbas3  13254  prdsdsval2  13257  invfuc  13692  yonedalem4c  13895  gsumconst  15044  prdsgsum  15064  dprdwd  15081  gsumdixp  15227  evlslem4  16077  elptr2  17101  ptunimpt  17122  ptcldmpt  17140  ptclsg  17141  txcnp  17146  ptcnplem  17147  cnmpt11  17189  cnmpt1t  17191  cnmptk2  17212  xkocnv  17337  flfcnp2  17534  iccpnfcnv  18274  ovolctb  18681  ovoliunlem1  18693  ovoliun2  18697  ovolshftlem1  18700  ovolscalem1  18704  voliun  18743  ioombl1lem3  18749  ioombl1lem4  18750  uniioombllem2  18770  mbfeqalem  18829  mbfpos  18838  mbfposr  18839  mbfposb  18840  mbfsup  18851  mbfinf  18852  mbflim  18855  i1fposd  18894  itg1climres  18901  mbfi1fseqlem4  18905  mbfi1fseqlem5  18906  mbfi1fseqlem6  18907  itg2split  18936  itg2mono  18940  itg2cnlem1  18948  isibl2  18953  itgmpt  18969  itgeqa  19000  itggt0  19028  itgcn  19029  limcmpt  19065  dvlipcn  19173  lhop2  19194  dvfsumabs  19202  itgparts  19226  itgsubstlem  19227  itgsubst  19228  elplyd  19416  coeeulem  19438  coeeq2  19456  dvply1  19496  plyremlem  19516  ulmss  19606  ulmdvlem1  19609  mtest  19613  itgulm2  19617  radcnvlem1  19621  pserulm  19630  leibpi  20070  rlimcnp  20092  o1cxp  20101  sqff1o  20252  lgseisenlem2  20421  dchrvmasumlem1  20476  ubthlem1  21279  cnlnadjlem5  22481  iscvm  22961  fprodadd  24518  fprodneg  24544  fprodsub  24545  trooo  24560  trinv  24561  ltrinvlem  24572  rltrooo  24581  svli2  24650  trnij  24781  cnegvex2  24826  rnegvex2  24827  mulmulvec  24853  distmlva  24854  distsava  24855  elrfirn2  25937  eq0rabdioph  26022  monotoddzz  26194  aomclem2  26318
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-mpt 3976  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fv 4608
  Copyright terms: Public domain W3C validator