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

Theorem fvmptg 5600
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 2283 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2294 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2289 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 2941 . . . 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 4079 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2303 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5599 . 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 1623    e. wcel 1684   E*wmo 2144   {copab 4076    e. cmpt 4077   ` cfv 5255
This theorem is referenced by:  fvmpti  5601  fvmpt  5602  fvmpts  5603  fvmpt3  5604  fvmptss2  5619  f1mpt  5785  undefval  6301  tz7.44-2  6420  tz7.44-3  6421  fvdiagfn  6812  resixpfo  6854  pw2f1olem  6966  fival  7166  wdom2d  7294  cantnfp1lem1  7380  cantnfp1lem2  7381  cantnfp1lem3  7382  wemapwe  7400  tz9.12lem3  7461  rankvalb  7469  cardval3  7585  cfval  7873  coftr  7899  fin23lem27  7954  isf34lem1  7998  fin1a2lem1  8026  fin1a2lem12  8037  axdc2lem  8074  pwcfsdom  8205  canthp1lem2  8275  wuncval  8364  tskmval  8461  climrlim2  12021  summolem3  12187  summolem2a  12188  iserodd  12888  divsfval  13449  mreacs  13560  pwsco1mhm  14446  pwsco2mhm  14447  vrmdfval  14478  galactghm  14783  efgtf  15031  gsummhm2  15212  dprdfid  15252  lspval  15732  aspval  16068  coe1tmfv1  16350  coe1tmfv2  16351  ply1sclid  16363  tgval  16693  cldval  16760  ntrfval  16761  clsfval  16762  ntrval  16773  clsval  16774  opncldf2  16822  opncldf3  16823  neifval  16836  neival  16839  lpfval  16870  lpval  16871  1stcfb  17171  cnmpt11  17357  cnmpt21  17365  cnmptkp  17374  cnmptk1p  17379  kqfval  17414  stdbdxmet  18061  cmetcaulem  18714  bcth3  18753  iunmbl  18910  itg2gt0  19115  ellimc2  19227  cnmptlimc  19240  limccnp  19241  limcco  19243  evlslem3  19398  coe1termlem  19639  coe1term  19640  ulmval  19759  pserulm  19798  rlimcnp  20260  xrlimcnp  20263  dchrelbasd  20478  grpoinvfval  20891  grpodivfval  20909  gxfval  20924  issubgo  20970  spanval  21912  nlfnval  22461  sigaval  23471  measval  23529  measdivcstOLD  23551  measdivcst  23552  probfinmeasbOLD  23631  ptpcon  23764  cvmsval  23797  dfrtrclrec2  24040  rtrclreclem.refl  24041  bdayval  24302  imageval  24469  fvimage  24470  mapmapmap  25148  injsurinj  25149  iscst1  25174  valcurfn1  25204  mxlelt  25264  mnlelt2  25266  fprod1i  25322  fprodp1  25323  trooo  25394  trinv  25395  ltrooo  25404  ltrinvlem  25406  islimrs  25580  supnufb  25630  sigadd  25649  isnullcv  25652  valvze  25654  addassv  25656  issubrv  25672  isucv  25677  ismulcv  25681  fnmulcv  25684  isdivcv2  25693  isinob  25862  isntr  25873  islimcat  25876  prismorcset  25914  morcatset1  25915  isgraphmrph  25923  domcatfun  25925  domcatval  25930  codcatfun  25934  codcatval  25936  idcatfun  25941  idmor  25946  isKleene  25988  pgapspf  26052  pgapspf2  26053  linevala2  26078  iscola2  26092  nds  26150  isside0  26164  islocfin  26296  tailfval  26321  tailval  26322  heiborlem4  26538  heiborlem6  26540  fvtresfn  26763  mzpval  26810  mzpsubst  26826  rabdiophlem2  26883  fphpdo  26900  monotoddzz  27028  pw2f1o2val  27132  dnnumch3lem  27143  pwssplit4  27191  uvcval  27234  uvcvval  27235  hbtlem1  27327  rgspnval  27373  pmtrval  27394  pmtrfv  27395  fmuldfeq  27713  stoweidlem31  27780  stoweidlem34  27783  lkrval  29278  pclvalN  30079  cdleme31fv  30579  docavalN  31313  dochval  31541  mapdval  31818  hvmapval  31950  hvmapvalvalN  31951  hdmap1vallem  31988  hdmapval  32021  hgmapval  32080
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263
  Copyright terms: Public domain W3C validator