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

Theorem fvmptg 5616
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
Allowed substitution hints:    B( x)    R( x)    F( x)

Proof of Theorem fvmptg
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eqid 2296 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2307 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2302 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 2954 . . . 4  |-  E* y 
y  =  B
65a1i 10 . . 3  |-  ( x  e.  D  ->  E* y  y  =  B
)
7 fvmptg.2 . . . 4  |-  F  =  ( x  e.  D  |->  B )
8 df-mpt 4095 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2316 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5615 . 2  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( C  =  C  ->  ( F `  A )  =  C ) )
111, 10mpi 16 1  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( F `  A
)  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696   E*wmo 2157   {copab 4092    e. cmpt 4093   ` cfv 5271
This theorem is referenced by:  fvmpti  5617  fvmpt  5618  fvmpts  5619  fvmpt3  5620  fvmptss2  5635  f1mpt  5801  undefval  6317  tz7.44-2  6436  tz7.44-3  6437  fvdiagfn  6828  resixpfo  6870  pw2f1olem  6982  fival  7182  wdom2d  7310  cantnfp1lem1  7396  cantnfp1lem2  7397  cantnfp1lem3  7398  wemapwe  7416  tz9.12lem3  7477  rankvalb  7485  cardval3  7601  cfval  7889  coftr  7915  fin23lem27  7970  isf34lem1  8014  fin1a2lem1  8042  fin1a2lem12  8053  axdc2lem  8090  pwcfsdom  8221  canthp1lem2  8291  wuncval  8380  tskmval  8477  climrlim2  12037  summolem3  12203  summolem2a  12204  iserodd  12904  divsfval  13465  mreacs  13576  pwsco1mhm  14462  pwsco2mhm  14463  vrmdfval  14494  galactghm  14799  efgtf  15047  gsummhm2  15228  dprdfid  15268  lspval  15748  aspval  16084  coe1tmfv1  16366  coe1tmfv2  16367  ply1sclid  16379  tgval  16709  cldval  16776  ntrfval  16777  clsfval  16778  ntrval  16789  clsval  16790  opncldf2  16838  opncldf3  16839  neifval  16852  neival  16855  lpfval  16886  lpval  16887  1stcfb  17187  cnmpt11  17373  cnmpt21  17381  cnmptkp  17390  cnmptk1p  17395  kqfval  17430  stdbdxmet  18077  cmetcaulem  18730  bcth3  18769  iunmbl  18926  itg2gt0  19131  ellimc2  19243  cnmptlimc  19256  limccnp  19257  limcco  19259  evlslem3  19414  coe1termlem  19655  coe1term  19656  ulmval  19775  pserulm  19814  rlimcnp  20276  xrlimcnp  20279  dchrelbasd  20494  grpoinvfval  20907  grpodivfval  20925  gxfval  20940  issubgo  20986  spanval  21928  nlfnval  22477  sigaval  23486  measval  23544  measdivcstOLD  23566  measdivcst  23567  probfinmeasbOLD  23646  ptpcon  23779  cvmsval  23812  dfrtrclrec2  24055  rtrclreclem.refl  24056  prodmolem3  24156  prodmolem2a  24157  bdayval  24373  imageval  24540  fvimage  24541  mapmapmap  25251  injsurinj  25252  iscst1  25277  valcurfn1  25307  mxlelt  25367  mnlelt2  25369  fprod1i  25425  fprodp1  25426  trooo  25497  trinv  25498  ltrooo  25507  ltrinvlem  25509  islimrs  25683  supnufb  25733  sigadd  25752  isnullcv  25755  valvze  25757  addassv  25759  issubrv  25775  isucv  25780  ismulcv  25784  fnmulcv  25787  isdivcv2  25796  isinob  25965  isntr  25976  islimcat  25979  prismorcset  26017  morcatset1  26018  isgraphmrph  26026  domcatfun  26028  domcatval  26033  codcatfun  26037  codcatval  26039  idcatfun  26044  idmor  26049  isKleene  26091  pgapspf  26155  pgapspf2  26156  linevala2  26181  iscola2  26195  nds  26253  isside0  26267  islocfin  26399  tailfval  26424  tailval  26425  heiborlem4  26641  heiborlem6  26643  fvtresfn  26866  mzpval  26913  mzpsubst  26929  rabdiophlem2  26986  fphpdo  27003  monotoddzz  27131  pw2f1o2val  27235  dnnumch3lem  27246  pwssplit4  27294  uvcval  27337  uvcvval  27338  hbtlem1  27430  rgspnval  27476  pmtrval  27497  pmtrfv  27498  fmuldfeq  27816  stoweidlem31  27883  stoweidlem34  27886  fargshiftfv  28380  lkrval  29900  pclvalN  30701  cdleme31fv  31201  docavalN  31935  dochval  32163  mapdval  32440  hvmapval  32572  hvmapvalvalN  32573  hdmap1vallem  32610  hdmapval  32643  hgmapval  32702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fv 5279
  Copyright terms: Public domain W3C validator