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

Theorem fvmptg 5743
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 2387 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2398 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2393 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 3053 . . . 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 4209 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2407 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5742 . 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 359    = wceq 1649    e. wcel 1717   E*wmo 2239   {copab 4206    e. cmpt 4207   ` cfv 5394
This theorem is referenced by:  fvmpti  5744  fvmpt  5745  fvmpts  5746  fvmpt3  5747  fvmptss2  5763  f1mpt  5946  undefval  6482  tz7.44-2  6601  tz7.44-3  6602  fvdiagfn  6994  resixpfo  7036  pw2f1olem  7148  fival  7352  wdom2d  7481  cantnfp1lem1  7567  cantnfp1lem2  7568  cantnfp1lem3  7569  wemapwe  7587  tz9.12lem3  7648  rankvalb  7656  cardval3  7772  cfval  8060  coftr  8086  fin23lem27  8141  isf34lem1  8185  fin1a2lem1  8213  fin1a2lem12  8224  axdc2lem  8261  pwcfsdom  8391  canthp1lem2  8461  wuncval  8550  tskmval  8647  climrlim2  12268  summolem3  12435  summolem2a  12436  iserodd  13136  divsfval  13699  mreacs  13810  pwsco1mhm  14696  pwsco2mhm  14697  vrmdfval  14728  galactghm  15033  efgtf  15281  gsummhm2  15462  dprdfid  15502  lspval  15978  aspval  16314  coe1tmfv1  16593  coe1tmfv2  16594  ply1sclid  16606  tgval  16943  cldval  17010  ntrfval  17011  clsfval  17012  ntrval  17023  clsval  17024  opncldf2  17072  opncldf3  17073  neifval  17086  neival  17089  lpfval  17125  lpval  17126  1stcfb  17429  cnmpt11  17616  cnmpt21  17624  cnmptkp  17633  cnmptk1p  17638  kqfval  17676  stdbdxmet  18435  cmetcaulem  19112  bcth3  19153  iunmbl  19314  itg2gt0  19519  ellimc2  19631  cnmptlimc  19644  limccnp  19645  limcco  19647  evlslem3  19802  coe1termlem  20043  coe1term  20044  ulmval  20163  pserulm  20205  rlimcnp  20671  xrlimcnp  20674  dchrelbasd  20890  nbgraf1olem4  21320  fargshiftfv  21470  grpoinvfval  21660  grpodivfval  21678  gxfval  21693  issubgo  21739  spanval  22683  nlfnval  23232  fvmpt2f  23914  sigaval  24289  measval  24348  measdivcstOLD  24372  measdivcst  24373  probfinmeasbOLD  24465  ptpcon  24699  cvmsval  24732  dfrtrclrec2  24922  rtrclreclem.refl  24923  climlec3  24993  prodmolem3  25038  prodmolem2a  25039  iprodmul  25088  bdayval  25326  imageval  25493  fvimage  25494  islocfin  26067  tailfval  26092  tailval  26093  heiborlem4  26214  heiborlem6  26216  fvtresfn  26435  mzpval  26480  mzpsubst  26496  rabdiophlem2  26553  fphpdo  26569  monotoddzz  26697  pw2f1o2val  26801  dnnumch3lem  26812  pwssplit4  26860  uvcval  26903  uvcvval  26904  hbtlem1  26996  rgspnval  27042  pmtrval  27063  pmtrfv  27064  refsum2cnlem1  27376  fmuldfeq  27381  stoweidlem26  27443  stoweidlem30  27447  stoweidlem31  27448  stoweidlem34  27451  stirlinglem5  27495  stirlinglem8  27498  lkrval  29203  pclvalN  30004  cdleme31fv  30504  docavalN  31238  dochval  31466  mapdval  31743  hvmapval  31875  hvmapvalvalN  31876  hdmap1vallem  31913  hdmapval  31946  hgmapval  32005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-iota 5358  df-fun 5396  df-fv 5402
  Copyright terms: Public domain W3C validator