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

Theorem fvmptg 6174
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 (𝑥 = 𝐴𝐵 = 𝐶)
fvmptg.2 𝐹 = (𝑥𝐷𝐵)
Assertion
Ref Expression
fvmptg ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝐹(𝑥)

Proof of Theorem fvmptg
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqid 2609 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2619 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2613 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3348 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4639 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2631 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6173 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  ∃*wmo 2458  {copab 4636  cmpt 4637  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fv 5798
This theorem is referenced by:  fvmpti  6175  fvmpt  6176  fvmpt2f  6177  fvtresfn  6178  fvmpts  6179  fvmpt3  6180  fvmptss2  6197  f1mpt  6397  undefval  7266  tz7.44-2  7367  tz7.44-3  7368  fvdiagfn  7765  resixpfo  7809  pw2f1olem  7926  fival  8178  wdom2d  8345  cantnfp1lem1  8435  cantnfp1lem2  8436  cantnfp1lem3  8437  wemapwe  8454  tz9.12lem3  8512  rankvalb  8520  cardval3  8638  cfval  8929  coftr  8955  fin23lem27  9010  isf34lem1  9054  fin1a2lem1  9082  fin1a2lem12  9093  axdc2lem  9130  pwcfsdom  9261  canthp1lem2  9331  wuncval  9420  tskmval  9517  lsw  13150  swrdswrd  13258  trclfv  13535  relexpsucnnr  13559  dfrtrclrec2  13591  rtrclreclem1  13592  climrlim2  14072  summolem3  14238  summolem2a  14239  prodmolem3  14448  prodmolem2a  14449  iprodmul  14519  iserodd  15324  divsfval  15976  mreacs  16088  joinfval  16770  meetfval  16784  pwsco1mhm  17139  pwsco2mhm  17140  vrmdfval  17162  galactghm  17592  symgextfv  17607  symgextfve  17608  symgfixfolem1  17627  pmtrval  17640  pmtrfv  17641  pmtrdifwrdel2lem1  17673  efgtf  17904  gsummhm2  18108  gsummpt1n0  18133  dprdfid  18185  lspval  18742  rrgsupp  19058  aspval  19095  evlslem3  19281  coe1tmfv1  19411  coe1tmfv2  19412  ply1sclid  19425  uvcval  19885  uvcvval  19886  marepvval  20134  submaval0  20147  m2detleiblem3  20196  m2detleiblem4  20197  maduval  20205  minmar1val0  20214  tgval  20512  cldval  20579  ntrfval  20580  clsfval  20581  ntrval  20592  clsval  20593  opncldf2  20641  opncldf3  20642  neifval  20655  neival  20658  lpfval  20694  lpval  20695  1stcfb  21000  islocfin  21072  cnmpt11  21218  cnmpt21  21226  cnmptkp  21235  cnmptk1p  21240  kqfval  21278  stdbdxmet  22071  cmetcaulem  22812  bcth3  22853  iunmbl  23045  itg2gt0  23250  ellimc2  23364  cnmptlimc  23377  limccnp  23378  limcco  23380  coe1termlem  23735  coe1term  23736  ulmval  23855  pserulm  23897  rlimcnp  24409  xrlimcnp  24412  dchrelbasd  24681  nbgraf1olem4  25739  fargshiftfv  25929  wwlkn  25976  clwwlkn  26061  clwlkfoclwwlk  26138  clwlkf1clwwlk  26143  rusgranumwlklem1  26242  usg2spot2nb  26358  usgreg2spot  26360  2spotmdisj  26361  usgreghash2spot  26362  numclwlk1lem2fv  26386  numclwlk2lem2fv  26397  grpoinvfval  26526  grpodivfval  26538  spanval  27382  nlfnval  27930  sigaval  29306  measval  29394  measdivcstOLD  29420  measdivcst  29421  probfinmeasbOLD  29623  ptpcon  30275  cvmsval  30308  climlec3  30678  bdayval  30851  imageval  31013  fvimage  31014  tailfval  31343  tailval  31344  bj-toponss  32037  bj-diagval  32063  curfv  32355  heiborlem4  32579  heiborlem6  32581  lkrval  33189  pclvalN  33990  cdleme31fv  34492  docavalN  35226  dochval  35454  mapdval  35731  hvmapval  35863  hvmapvalvalN  35864  hdmap1vallem  35901  hdmapval  35934  hgmapval  35993  mzpval  36109  mzpsubst  36125  rabdiophlem2  36180  fphpdo  36195  monotoddzz  36322  pw2f1o2val  36420  dnnumch3lem  36430  pwssplit4  36473  hbtlem1  36508  rgspnval  36553  eliunov2  36786  fvmptiunrelexplb0d  36791  fvmptiunrelexplb1d  36793  refsum2cnlem1  38015  fmuldfeq  38447  cncfiooicclem1  38576  stoweidlem26  38716  stoweidlem30  38720  stoweidlem31  38721  stoweidlem34  38724  stirlinglem5  38768  stirlinglem8  38771  fourierdlem50  38846  sge0snmptf  39127  caragenval  39180  clwlksfoclwwlk  41265  clwlksf1clwwlk  41271  fusgr2wsp2nb  41493  fusgreg2wsp  41495  lincvalsc0  41999  linc0scn0  42001  linc1  42003  lincscm  42008  el0ldep  42044
  Copyright terms: Public domain W3C validator