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

Theorem fvmptg 5806
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 2438 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2449 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2444 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 3112 . . . 4  |-  E* y 
y  =  B
65a1i 11 . . 3  |-  ( x  e.  D  ->  E* y  y  =  B
)
7 fvmptg.2 . . . 4  |-  F  =  ( x  e.  D  |->  B )
8 df-mpt 4270 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2458 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5805 . 2  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( C  =  C  ->  ( F `  A )  =  C ) )
111, 10mpi 17 1  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( F `  A
)  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   E*wmo 2284   {copab 4267    e. cmpt 4268   ` cfv 5456
This theorem is referenced by:  fvmpti  5807  fvmpt  5808  fvmpts  5809  fvmpt3  5810  fvmptss2  5826  f1mpt  6009  undefval  6548  tz7.44-2  6667  tz7.44-3  6668  fvdiagfn  7060  resixpfo  7102  pw2f1olem  7214  fival  7419  wdom2d  7550  cantnfp1lem1  7636  cantnfp1lem2  7637  cantnfp1lem3  7638  wemapwe  7656  tz9.12lem3  7717  rankvalb  7725  cardval3  7841  cfval  8129  coftr  8155  fin23lem27  8210  isf34lem1  8254  fin1a2lem1  8282  fin1a2lem12  8293  axdc2lem  8330  pwcfsdom  8460  canthp1lem2  8530  wuncval  8619  tskmval  8716  climrlim2  12343  summolem3  12510  summolem2a  12511  iserodd  13211  divsfval  13774  mreacs  13885  pwsco1mhm  14771  pwsco2mhm  14772  vrmdfval  14803  galactghm  15108  efgtf  15356  gsummhm2  15537  dprdfid  15577  lspval  16053  aspval  16389  coe1tmfv1  16668  coe1tmfv2  16669  ply1sclid  16681  tgval  17022  cldval  17089  ntrfval  17090  clsfval  17091  ntrval  17102  clsval  17103  opncldf2  17151  opncldf3  17152  neifval  17165  neival  17168  lpfval  17204  lpval  17205  1stcfb  17510  cnmpt11  17697  cnmpt21  17705  cnmptkp  17714  cnmptk1p  17719  kqfval  17757  stdbdxmet  18547  cmetcaulem  19243  bcth3  19286  iunmbl  19449  itg2gt0  19654  ellimc2  19766  cnmptlimc  19779  limccnp  19780  limcco  19782  evlslem3  19937  coe1termlem  20178  coe1term  20179  ulmval  20298  pserulm  20340  rlimcnp  20806  xrlimcnp  20809  dchrelbasd  21025  nbgraf1olem4  21456  fargshiftfv  21624  grpoinvfval  21814  grpodivfval  21832  gxfval  21847  issubgo  21893  spanval  22837  nlfnval  23386  fvmpt2f  24074  sigaval  24495  measval  24554  measdivcstOLD  24580  measdivcst  24581  probfinmeasbOLD  24688  ptpcon  24922  cvmsval  24955  dfrtrclrec2  25145  rtrclreclem.refl  25146  climlec3  25216  prodmolem3  25261  prodmolem2a  25262  iprodmul  25318  bdayval  25605  imageval  25777  fvimage  25778  islocfin  26378  tailfval  26403  tailval  26404  heiborlem4  26525  heiborlem6  26527  fvtresfn  26746  mzpval  26791  mzpsubst  26807  rabdiophlem2  26864  fphpdo  26880  monotoddzz  27008  pw2f1o2val  27112  dnnumch3lem  27123  pwssplit4  27170  uvcval  27213  uvcvval  27214  hbtlem1  27306  rgspnval  27352  pmtrval  27373  pmtrfv  27374  refsum2cnlem1  27686  fmuldfeq  27691  stoweidlem26  27753  stoweidlem30  27757  stoweidlem31  27758  stoweidlem34  27761  stirlinglem5  27805  stirlinglem8  27808  swrdswrd  28221  lswrd  28281  wwlkn  28352  usg2spot2nb  28516  usgreg2spot  28518  2spotmdisj  28519  usgreghash2spot  28520  lkrval  29948  pclvalN  30749  cdleme31fv  31249  docavalN  31983  dochval  32211  mapdval  32488  hvmapval  32620  hvmapvalvalN  32621  hdmap1vallem  32658  hdmapval  32691  hgmapval  32750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-iota 5420  df-fun 5458  df-fv 5464
  Copyright terms: Public domain W3C validator