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

Theorem fvmptg 5767
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 2408 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2419 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2414 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 3074 . . . 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 4232 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2428 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5766 . 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 1721   E*wmo 2259   {copab 4229    e. cmpt 4230   ` cfv 5417
This theorem is referenced by:  fvmpti  5768  fvmpt  5769  fvmpts  5770  fvmpt3  5771  fvmptss2  5787  f1mpt  5970  undefval  6509  tz7.44-2  6628  tz7.44-3  6629  fvdiagfn  7021  resixpfo  7063  pw2f1olem  7175  fival  7379  wdom2d  7508  cantnfp1lem1  7594  cantnfp1lem2  7595  cantnfp1lem3  7596  wemapwe  7614  tz9.12lem3  7675  rankvalb  7683  cardval3  7799  cfval  8087  coftr  8113  fin23lem27  8168  isf34lem1  8212  fin1a2lem1  8240  fin1a2lem12  8251  axdc2lem  8288  pwcfsdom  8418  canthp1lem2  8488  wuncval  8577  tskmval  8674  climrlim2  12300  summolem3  12467  summolem2a  12468  iserodd  13168  divsfval  13731  mreacs  13842  pwsco1mhm  14728  pwsco2mhm  14729  vrmdfval  14760  galactghm  15065  efgtf  15313  gsummhm2  15494  dprdfid  15534  lspval  16010  aspval  16346  coe1tmfv1  16625  coe1tmfv2  16626  ply1sclid  16638  tgval  16979  cldval  17046  ntrfval  17047  clsfval  17048  ntrval  17059  clsval  17060  opncldf2  17108  opncldf3  17109  neifval  17122  neival  17125  lpfval  17161  lpval  17162  1stcfb  17465  cnmpt11  17652  cnmpt21  17660  cnmptkp  17669  cnmptk1p  17674  kqfval  17712  stdbdxmet  18502  cmetcaulem  19198  bcth3  19241  iunmbl  19404  itg2gt0  19609  ellimc2  19721  cnmptlimc  19734  limccnp  19735  limcco  19737  evlslem3  19892  coe1termlem  20133  coe1term  20134  ulmval  20253  pserulm  20295  rlimcnp  20761  xrlimcnp  20764  dchrelbasd  20980  nbgraf1olem4  21411  fargshiftfv  21579  grpoinvfval  21769  grpodivfval  21787  gxfval  21802  issubgo  21848  spanval  22792  nlfnval  23341  fvmpt2f  24029  sigaval  24450  measval  24509  measdivcstOLD  24535  measdivcst  24536  probfinmeasbOLD  24643  ptpcon  24877  cvmsval  24910  dfrtrclrec2  25100  rtrclreclem.refl  25101  climlec3  25171  prodmolem3  25216  prodmolem2a  25217  iprodmul  25273  bdayval  25520  imageval  25687  fvimage  25688  islocfin  26270  tailfval  26295  tailval  26296  heiborlem4  26417  heiborlem6  26419  fvtresfn  26638  mzpval  26683  mzpsubst  26699  rabdiophlem2  26756  fphpdo  26772  monotoddzz  26900  pw2f1o2val  27004  dnnumch3lem  27015  pwssplit4  27063  uvcval  27106  uvcvval  27107  hbtlem1  27199  rgspnval  27245  pmtrval  27266  pmtrfv  27267  refsum2cnlem1  27579  fmuldfeq  27584  stoweidlem26  27646  stoweidlem30  27650  stoweidlem31  27651  stoweidlem34  27654  stirlinglem5  27698  stirlinglem8  27701  swrdswrd  28015  usg2spot2nb  28172  usgreg2spot  28174  2spotmdisj  28175  usgreghash2spot  28176  lkrval  29575  pclvalN  30376  cdleme31fv  30876  docavalN  31610  dochval  31838  mapdval  32115  hvmapval  32247  hvmapvalvalN  32248  hdmap1vallem  32285  hdmapval  32318  hgmapval  32377
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 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
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 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-iota 5381  df-fun 5419  df-fv 5425
  Copyright terms: Public domain W3C validator