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  ptpcon  23175  cvmsval  23208  dfrtrclrec2  23451  rtrclreclem.refl  23452  bdayval  23713  imageval  23880  fvimage  23881  mapmapmap  24560  injsurinj  24561  iscst1  24586  valcurfn1  24616  mxlelt  24676  mnlelt2  24678  fprod1i  24734  fprodp1  24735  trooo  24806  trinv  24807  ltrooo  24816  ltrinvlem  24818  islimrs  24992  supnufb  25042  sigadd  25061  isnullcv  25064  valvze  25066  addassv  25068  issubrv  25084  isucv  25089  ismulcv  25093  fnmulcv  25096  isdivcv2  25105  isinob  25274  isntr  25285  islimcat  25288  prismorcset  25326  morcatset1  25327  isgraphmrph  25335  domcatfun  25337  domcatval  25342  codcatfun  25346  codcatval  25348  idcatfun  25353  idmor  25358  isKleene  25400  pgapspf  25464  pgapspf2  25465  linevala2  25490  iscola2  25504  nds  25562  isside0  25576  islocfin  25708  tailfval  25733  tailval  25734  heiborlem4  25950  heiborlem6  25952  fvtresfn  26175  mzpval  26222  mzpsubst  26238  rabdiophlem2  26295  fphpdo  26312  monotoddzz  26440  pw2f1o2val  26544  dnnumch3lem  26555  pwssplit4  26603  uvcval  26646  uvcvval  26647  hbtlem1  26739  rgspnval  26785  pmtrval  26806  pmtrfv  26807  fmuldfeq  27125  stoweidlem31  27192  stoweidlem34  27195  lkrval  28651  pclvalN  29452  cdleme31fv  29952  docavalN  30686  dochval  30914  mapdval  31191  hvmapval  31323  hvmapvalvalN  31324  hdmap1vallem  31361  hdmapval  31394  hgmapval  31453
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-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