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

Theorem fvmptg 6237
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 2621 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2631 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2625 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3364 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4675 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2643 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6235 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  ∃*wmo 2470  {copab 4672  cmpt 4673  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855
This theorem is referenced by:  fvmpti  6238  fvmpt  6239  fvmpt2f  6240  fvtresfn  6241  fvmpts  6242  fvmpt3  6243  fvmptss2  6260  f1mpt  6472  undefval  7347  tz7.44-2  7448  tz7.44-3  7449  fvdiagfn  7846  resixpfo  7890  pw2f1olem  8008  fival  8262  wdom2d  8429  cantnfp1lem1  8519  cantnfp1lem2  8520  cantnfp1lem3  8521  wemapwe  8538  tz9.12lem3  8596  rankvalb  8604  cardval3  8722  cfval  9013  coftr  9039  fin23lem27  9094  isf34lem1  9138  fin1a2lem1  9166  fin1a2lem12  9177  axdc2lem  9214  pwcfsdom  9349  canthp1lem2  9419  wuncval  9508  tskmval  9605  lsw  13290  swrdswrd  13398  trclfv  13675  relexpsucnnr  13699  dfrtrclrec2  13731  rtrclreclem1  13732  climrlim2  14212  summolem3  14378  summolem2a  14379  prodmolem3  14588  prodmolem2a  14589  iprodmul  14659  iserodd  15464  divsfval  16128  mreacs  16240  joinfval  16922  meetfval  16936  pwsco1mhm  17291  pwsco2mhm  17292  vrmdfval  17314  galactghm  17744  symgextfv  17759  symgextfve  17760  symgfixfolem1  17779  pmtrval  17792  pmtrfv  17793  pmtrdifwrdel2lem1  17825  efgtf  18056  gsummhm2  18260  gsummpt1n0  18285  dprdfid  18337  lspval  18894  rrgsupp  19210  aspval  19247  evlslem3  19433  coe1tmfv1  19563  coe1tmfv2  19564  ply1sclid  19577  uvcval  20043  uvcvval  20044  marepvval  20292  submaval0  20305  m2detleiblem3  20354  m2detleiblem4  20355  maduval  20363  minmar1val0  20372  tgval  20670  cldval  20737  ntrfval  20738  clsfval  20739  ntrval  20750  clsval  20751  opncldf2  20799  opncldf3  20800  neifval  20813  neival  20816  lpfval  20852  lpval  20853  1stcfb  21158  islocfin  21230  cnmpt11  21376  cnmpt21  21384  cnmptkp  21393  cnmptk1p  21398  kqfval  21436  stdbdxmet  22230  cmetcaulem  22994  bcth3  23036  iunmbl  23228  itg2gt0  23433  ellimc2  23547  cnmptlimc  23560  limccnp  23561  limcco  23563  coe1termlem  23918  coe1term  23919  ulmval  24038  pserulm  24080  rlimcnp  24592  xrlimcnp  24595  dchrelbasd  24864  clwlksfoclwwlk  26829  clwlksf1clwwlk  26835  fusgr2wsp2nb  27056  fusgreg2wsp  27058  grpoinvfval  27222  grpodivfval  27234  spanval  28038  nlfnval  28586  sigaval  29951  measval  30039  measdivcstOLD  30065  measdivcst  30066  probfinmeasbOLD  30268  ptpconn  30920  cvmsval  30953  climlec3  31324  bdayval  31499  imageval  31676  fvimage  31677  tailfval  32006  tailval  32007  bj-toponss  32694  bj-diagval  32720  curfv  33018  heiborlem4  33242  heiborlem6  33244  lkrval  33852  pclvalN  34653  cdleme31fv  35155  docavalN  35889  dochval  36117  mapdval  36394  hvmapval  36526  hvmapvalvalN  36527  hdmap1vallem  36564  hdmapval  36597  hgmapval  36656  mzpval  36772  mzpsubst  36788  rabdiophlem2  36843  fphpdo  36858  monotoddzz  36985  pw2f1o2val  37083  dnnumch3lem  37093  pwssplit4  37136  hbtlem1  37171  rgspnval  37216  eliunov2  37449  fvmptiunrelexplb0d  37454  fvmptiunrelexplb1d  37456  refsum2cnlem1  38676  fmuldfeq  39216  cncfiooicclem1  39407  stoweidlem26  39547  stoweidlem30  39551  stoweidlem31  39552  stoweidlem34  39555  stirlinglem5  39599  stirlinglem8  39602  fourierdlem50  39677  sge0snmptf  39958  caragenval  40011  fargshiftfv  40670  lincvalsc0  41495  linc0scn0  41497  linc1  41499  lincscm  41504  el0ldep  41540
  Copyright terms: Public domain W3C validator