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

Theorem fvmptg 5561
Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptg.1  |-  ( x  =  A  ->  B  =  C )
fvmptg.2  |-  F  =  ( x  e.  D  |->  B )
Assertion
Ref Expression
fvmptg  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( F `  A
)  =  C )
Distinct variable groups:    x, A    x, C    x, D
Dummy variable  y is distinct from all other variables.
Allowed substitution hints:    B( x)    R( x)    F( x)

Proof of Theorem fvmptg
StepHypRef Expression
1 eqid 2284 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2295 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2290 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 2942 . . . 4  |-  E* y 
y  =  B
65a1i 12 . . 3  |-  ( x  e.  D  ->  E* y  y  =  B
)
7 fvmptg.2 . . . 4  |-  F  =  ( x  e.  D  |->  B )
8 df-mpt 4080 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2304 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5560 . 2  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( C  =  C  ->  ( F `  A )  =  C ) )
111, 10mpi 18 1  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( F `  A
)  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   E*wmo 2145   {copab 4077    e. cmpt 4078   ` cfv 5221
This theorem is referenced by:  fvmpti  5562  fvmpt  5563  fvmpts  5564  fvmpt3  5565  fvmptss2  5580  f1mpt  5746  undefval  6296  tz7.44-2  6415  tz7.44-3  6416  fvdiagfn  6807  resixpfo  6849  pw2f1olem  6961  fival  7161  wdom2d  7289  cantnfp1lem1  7375  cantnfp1lem2  7376  cantnfp1lem3  7377  wemapwe  7395  tz9.12lem3  7456  rankvalb  7464  cardval3  7580  cfval  7868  coftr  7894  fin23lem27  7949  isf34lem1  7993  fin1a2lem1  8021  fin1a2lem12  8032  axdc2lem  8069  pwcfsdom  8200  canthp1lem2  8270  wuncval  8359  tskmval  8456  climrlim2  12015  summolem3  12181  summolem2a  12182  iserodd  12882  divsfval  13443  mreacs  13554  pwsco1mhm  14440  pwsco2mhm  14441  vrmdfval  14472  galactghm  14777  efgtf  15025  gsummhm2  15206  dprdfid  15246  lspval  15726  aspval  16062  coe1tmfv1  16344  coe1tmfv2  16345  ply1sclid  16357  tgval  16687  cldval  16754  ntrfval  16755  clsfval  16756  ntrval  16767  clsval  16768  opncldf2  16816  opncldf3  16817  neifval  16830  neival  16833  lpfval  16864  lpval  16865  1stcfb  17165  cnmpt11  17351  cnmpt21  17359  cnmptkp  17368  cnmptk1p  17373  kqfval  17408  stdbdxmet  18055  cmetcaulem  18708  bcth3  18747  iunmbl  18904  itg2gt0  19109  ellimc2  19221  cnmptlimc  19234  limccnp  19235  limcco  19237  evlslem3  19392  coe1termlem  19633  coe1term  19634  ulmval  19753  pserulm  19792  rlimcnp  20254  xrlimcnp  20257  dchrelbasd  20472  grpoinvfval  20883  grpodivfval  20901  gxfval  20916  issubgo  20962  spanval  21904  nlfnval  22453  ptpcon  23168  cvmsval  23201  dfrtrclrec2  23444  rtrclreclem.refl  23445  bdayval  23703  imageval  23876  fvimage  23877  mapmapmap  24547  injsurinj  24548  iscst1  24573  valcurfn1  24603  mxlelt  24663  mnlelt2  24665  fprod1i  24721  fprodp1  24722  trooo  24793  trinv  24794  ltrooo  24803  ltrinvlem  24805  islimrs  24979  supnufb  25029  sigadd  25048  isnullcv  25051  valvze  25053  addassv  25055  issubrv  25071  isucv  25076  ismulcv  25080  fnmulcv  25083  isdivcv2  25092  isinob  25261  isntr  25272  islimcat  25275  prismorcset  25313  morcatset1  25314  isgraphmrph  25322  domcatfun  25324  domcatval  25329  codcatfun  25333  codcatval  25335  idcatfun  25340  idmor  25345  isKleene  25387  pgapspf  25451  pgapspf2  25452  linevala2  25477  iscola2  25491  nds  25549  isside0  25563  islocfin  25695  tailfval  25720  tailval  25721  heiborlem4  25937  heiborlem6  25939  fvtresfn  26162  mzpval  26209  mzpsubst  26225  rabdiophlem2  26282  fphpdo  26299  monotoddzz  26427  pw2f1o2val  26531  dnnumch3lem  26542  pwssplit4  26590  uvcval  26633  uvcvval  26634  hbtlem1  26726  rgspnval  26772  pmtrval  26793  pmtrfv  26794  fmuldfeq  27112  stoweidlem31  27179  stoweidlem34  27182  lkrval  28545  pclvalN  29346  cdleme31fv  29846  docavalN  30580  dochval  30808  mapdval  31085  hvmapval  31217  hvmapvalvalN  31218  hdmap1vallem  31255  hdmapval  31288  hgmapval  31347
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fv 5229
  Copyright terms: Public domain W3C validator