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

Theorem fvmptg 5534
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 2258 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2269 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2264 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 2916 . . . 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 4053 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2278 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5533 . 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 2119   {copab 4050    e. cmpt 4051   ` cfv 4673
This theorem is referenced by:  fvmpti  5535  fvmpt  5536  fvmpts  5537  fvmpt3  5538  fvmptss2  5553  f1mpt  5719  undefval  6269  tz7.44-2  6388  tz7.44-3  6389  fvdiagfn  6780  resixpfo  6822  pw2f1olem  6934  fival  7134  wdom2d  7262  cantnfp1lem1  7348  cantnfp1lem2  7349  cantnfp1lem3  7350  wemapwe  7368  tz9.12lem3  7429  rankvalb  7437  cardval3  7553  cfval  7841  coftr  7867  fin23lem27  7922  isf34lem1  7966  fin1a2lem1  7994  fin1a2lem12  8005  axdc2lem  8042  pwcfsdom  8173  canthp1lem2  8243  wuncval  8332  tskmval  8429  climrlim2  11986  summolem3  12152  summolem2a  12153  iserodd  12850  divsfval  13411  mreacs  13522  pwsco1mhm  14408  pwsco2mhm  14409  vrmdfval  14440  galactghm  14745  efgtf  14993  gsummhm2  15174  dprdfid  15214  lspval  15694  aspval  16030  coe1tmfv1  16312  coe1tmfv2  16313  ply1sclid  16325  tgval  16655  cldval  16722  ntrfval  16723  clsfval  16724  ntrval  16735  clsval  16736  opncldf2  16784  opncldf3  16785  neifval  16798  neival  16801  lpfval  16832  lpval  16833  1stcfb  17133  cnmpt11  17319  cnmpt21  17327  cnmptkp  17336  cnmptk1p  17341  kqfval  17376  stdbdxmet  18023  cmetcaulem  18676  bcth3  18715  iunmbl  18872  itg2gt0  19077  ellimc2  19189  cnmptlimc  19202  limccnp  19203  limcco  19205  evlslem3  19360  coe1termlem  19601  coe1term  19602  ulmval  19721  pserulm  19760  rlimcnp  20222  xrlimcnp  20225  dchrelbasd  20440  grpoinvfval  20851  grpodivfval  20869  gxfval  20884  issubgo  20930  spanval  21872  nlfnval  22421  ptpcon  23136  cvmsval  23169  dfrtrclrec2  23412  rtrclreclem.refl  23413  bdayval  23671  imageval  23844  fvimage  23845  mapmapmap  24515  injsurinj  24516  iscst1  24541  valcurfn1  24571  mxlelt  24631  mnlelt2  24633  fprod1i  24689  fprodp1  24690  trooo  24761  trinv  24762  ltrooo  24771  ltrinvlem  24773  islimrs  24947  supnufb  24997  sigadd  25016  isnullcv  25019  valvze  25021  addassv  25023  issubrv  25039  isucv  25044  ismulcv  25048  fnmulcv  25051  isdivcv2  25060  isinob  25229  isntr  25240  islimcat  25243  prismorcset  25281  morcatset1  25282  isgraphmrph  25290  domcatfun  25292  domcatval  25297  codcatfun  25301  codcatval  25303  idcatfun  25308  idmor  25313  isKleene  25355  pgapspf  25419  pgapspf2  25420  linevala2  25445  iscola2  25459  nds  25517  isside0  25531  islocfin  25663  tailfval  25688  tailval  25689  heiborlem4  25905  heiborlem6  25907  fvtresfn  26130  mzpval  26177  mzpsubst  26193  rabdiophlem2  26250  fphpdo  26267  monotoddzz  26395  pw2f1o2val  26499  dnnumch3lem  26510  pwssplit4  26558  uvcval  26601  uvcvval  26602  hbtlem1  26694  rgspnval  26740  pmtrval  26761  pmtrfv  26762  fmuldfeq  27081  stoweidlem31  27115  stoweidlem34  27118  lkrval  28445  pclvalN  29246  cdleme31fv  29746  docavalN  30480  dochval  30708  mapdval  30985  hvmapval  31117  hvmapvalvalN  31118  hdmap1vallem  31155  hdmapval  31188  hgmapval  31247
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 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
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 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-mpt 4053  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fv 4689
  Copyright terms: Public domain W3C validator