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

Theorem fvmpt2 5542
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 5541 . 2  |-  ( x  e.  A  ->  ( F `  x )  =  (  _I  `  B
) )
3 fvi 5513 . 2  |-  ( B  e.  C  ->  (  _I  `  B )  =  B )
42, 3sylan9eq 2310 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 4051    _I cid 4276   ` cfv 4673
This theorem is referenced by:  fvmptss  5543  fvmptdf  5545  mpteqb  5548  fvmptt  5549  fvmptf  5550  ralrnmpt  5603  fmptco  5625  f1mpt  5719  offval2  6029  ofrfval2  6030  mptelixpg  6821  dom2lem  6869  mapxpen  6995  xpmapenlem  6996  cnfcom3clem  7376  tcvalg  7391  rankf  7434  infxpenc2lem2  7615  dfac8clem  7627  acni2  7641  acnlem  7643  fin23lem32  7938  axcc2lem  8030  axcc3  8032  domtriomlem  8036  ac6num  8074  konigthlem  8158  rpnnen1lem1  10309  rpnnen1lem3  10311  rpnnen1lem5  10313  seqof  11069  rlim2  11935  ello1mpt  11960  o1compt  12026  sumrblem  12149  fsumcvg  12150  summolem2a  12153  zsum  12156  fsum  12158  fsumcvg2  12165  fsumadd  12176  isummulc2  12190  fsummulc2  12211  fsumrelem  12230  iserodd  12850  prmrec  12931  prdsbas3  13342  prdsdsval2  13345  invfuc  13810  yonedalem4c  14013  gsumconst  15171  prdsgsum  15191  dprdwd  15208  gsumdixp  15354  evlslem4  16207  elptr2  17231  ptunimpt  17252  ptcldmpt  17270  ptclsg  17271  txcnp  17276  ptcnplem  17277  cnmpt11  17319  cnmpt1t  17321  cnmptk2  17342  xkocnv  17467  flfcnp2  17664  iccpnfcnv  18404  ovolctb  18811  ovoliunlem1  18823  ovoliun2  18827  ovolshftlem1  18830  ovolscalem1  18834  voliun  18873  ioombl1lem3  18879  ioombl1lem4  18880  uniioombllem2  18900  mbfeqalem  18959  mbfpos  18968  mbfposr  18969  mbfposb  18970  mbfsup  18981  mbfinf  18982  mbflim  18985  i1fposd  19024  itg1climres  19031  mbfi1fseqlem4  19035  mbfi1fseqlem5  19036  mbfi1fseqlem6  19037  itg2split  19066  itg2mono  19070  itg2cnlem1  19078  isibl2  19083  itgmpt  19099  itgeqa  19130  itggt0  19158  itgcn  19159  limcmpt  19195  dvlipcn  19303  lhop2  19324  dvfsumabs  19332  itgparts  19356  itgsubstlem  19357  itgsubst  19358  elplyd  19546  coeeulem  19568  coeeq2  19586  dvply1  19626  plyremlem  19646  ulmss  19736  ulmdvlem1  19739  mtest  19743  itgulm2  19747  radcnvlem1  19751  pserulm  19760  leibpi  20200  rlimcnp  20222  o1cxp  20231  sqff1o  20382  lgseisenlem2  20551  dchrvmasumlem1  20606  ubthlem1  21409  cnlnadjlem5  22611  iscvm  23162  fprodadd  24719  fprodneg  24745  fprodsub  24746  trooo  24761  trinv  24762  ltrinvlem  24773  rltrooo  24782  svli2  24851  trnij  24982  cnegvex2  25027  rnegvex2  25028  mulmulvec  25054  distmlva  25055  distsava  25056  elrfirn2  26138  eq0rabdioph  26223  monotoddzz  26395  aomclem2  26519  refsumcn  27069  refsum2cnlem1  27076  fmuldfeqlem1  27080  fmuldfeq  27081  stoweidlem2  27086  stoweidlem11  27095  stoweidlem12  27096  stoweidlem16  27100  stoweidlem17  27101  stoweidlem18  27102  stoweidlem19  27103  stoweidlem20  27104  stoweidlem21  27105  stoweidlem22  27106  stoweidlem23  27107  stoweidlem27  27111  stoweidlem31  27115  stoweidlem34  27118  stoweidlem36  27120  stoweidlem40  27124  stoweidlem41  27125  stoweidlem42  27126  stoweidlem48  27132  stoweidlem51  27135  stoweidlem55  27139  stoweidlem59  27143  stoweidlem62  27146
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 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
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 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-mpt 4053  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fv 4689
  Copyright terms: Public domain W3C validator