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

Theorem fvmptg 5452
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
StepHypRef Expression
1 eqid 2253 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2264 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2259 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 2878 . . . 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 3976 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2273 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5451 . 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 1619    e. wcel 1621   E*wmo 2115   {copab 3973    e. cmpt 3974   ` cfv 4592
This theorem is referenced by:  fvmpti  5453  fvmpt  5454  fvmpts  5455  fvmpt3  5456  fvmptss2  5471  f1mpt  5637  undefval  6187  tz7.44-2  6306  tz7.44-3  6307  fvdiagfn  6698  resixpfo  6740  pw2f1olem  6851  fival  7050  wdom2d  7178  cantnfp1lem1  7264  cantnfp1lem2  7265  cantnfp1lem3  7266  wemapwe  7284  tz9.12lem3  7345  rankvalb  7353  cardval3  7469  cfval  7757  coftr  7783  fin23lem27  7838  isf34lem1  7882  fin1a2lem1  7910  fin1a2lem12  7921  axdc2lem  7958  pwcfsdom  8085  canthp1lem2  8155  wuncval  8244  tskmval  8341  climrlim2  11898  summolem3  12064  summolem2a  12065  iserodd  12762  divsfval  13323  mreacs  13404  pwsco1mhm  14281  pwsco2mhm  14282  vrmdfval  14313  galactghm  14618  efgtf  14866  gsummhm2  15047  dprdfid  15087  lspval  15567  aspval  15900  coe1tmfv1  16182  coe1tmfv2  16183  ply1sclid  16195  tgval  16525  cldval  16592  ntrfval  16593  clsfval  16594  ntrval  16605  clsval  16606  opncldf2  16654  opncldf3  16655  neifval  16668  neival  16671  lpfval  16702  lpval  16703  1stcfb  17003  cnmpt11  17189  cnmpt21  17197  cnmptkp  17206  cnmptk1p  17211  kqfval  17246  stdbdxmet  17893  cmetcaulem  18546  bcth3  18585  iunmbl  18742  itg2gt0  18947  ellimc2  19059  cnmptlimc  19072  limccnp  19073  limcco  19075  evlslem3  19230  coe1termlem  19471  coe1term  19472  ulmval  19591  pserulm  19630  rlimcnp  20092  xrlimcnp  20095  dchrelbasd  20310  grpoinvfval  20721  grpodivfval  20739  gxfval  20754  issubgo  20800  spanval  21742  nlfnval  22291  ptpcon  22935  cvmsval  22968  dfrtrclrec2  23211  rtrclreclem.refl  23212  bdayval  23470  imageval  23643  fvimage  23644  mapmapmap  24314  injsurinj  24315  iscst1  24340  valcurfn1  24370  mxlelt  24430  mnlelt2  24432  fprod1i  24488  fprodp1  24489  trooo  24560  trinv  24561  ltrooo  24570  ltrinvlem  24572  islimrs  24746  supnufb  24796  sigadd  24815  isnullcv  24818  valvze  24820  addassv  24822  issubrv  24838  isucv  24843  ismulcv  24847  fnmulcv  24850  isdivcv2  24859  isinob  25028  isntr  25039  islimcat  25042  prismorcset  25080  morcatset1  25081  isgraphmrph  25089  domcatfun  25091  domcatval  25096  codcatfun  25100  codcatval  25102  idcatfun  25107  idmor  25112  isKleene  25154  pgapspf  25218  pgapspf2  25219  linevala2  25244  iscola2  25258  nds  25316  isside0  25330  islocfin  25462  tailfval  25487  tailval  25488  heiborlem4  25704  heiborlem6  25706  fvtresfn  25929  mzpval  25976  mzpsubst  25992  rabdiophlem2  26049  fphpdo  26066  monotoddzz  26194  pw2f1o2val  26298  dnnumch3lem  26309  pwssplit4  26357  uvcval  26400  uvcvval  26401  hbtlem1  26493  rgspnval  26539  pmtrval  26560  pmtrfv  26561  lkrval  27967  pclvalN  28768  cdleme31fv  29268  docavalN  30002  dochval  30230  mapdval  30507  hvmapval  30639  hvmapvalvalN  30640  hdmap1vallem  30677  hdmapval  30710  hgmapval  30769
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-mpt 3976  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fv 4608
  Copyright terms: Public domain W3C validator