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

Theorem fvmptg 6267
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 2620 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2630 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2624 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3376 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4721 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2642 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6265 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wcel 1988  ∃*wmo 2469  {copab 4703  cmpt 4720  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fv 5884
This theorem is referenced by:  fvmpti  6268  fvmpt  6269  fvmpt2f  6270  fvtresfn  6271  fvmpts  6272  fvmpt3  6273  fvmptss2  6290  f1mpt  6503  undefval  7387  tz7.44-2  7488  tz7.44-3  7489  fvdiagfn  7887  resixpfo  7931  pw2f1olem  8049  fival  8303  wdom2d  8470  cantnfp1lem1  8560  cantnfp1lem2  8561  cantnfp1lem3  8562  wemapwe  8579  tz9.12lem3  8637  rankvalb  8645  cardval3  8763  cfval  9054  coftr  9080  fin23lem27  9135  isf34lem1  9179  fin1a2lem1  9207  fin1a2lem12  9218  axdc2lem  9255  pwcfsdom  9390  canthp1lem2  9460  wuncval  9549  tskmval  9646  lsw  13334  swrdswrd  13442  trclfv  13722  relexpsucnnr  13746  dfrtrclrec2  13778  rtrclreclem1  13779  climrlim2  14259  summolem3  14426  summolem2a  14427  prodmolem3  14644  prodmolem2a  14645  iprodmul  14715  iserodd  15521  divsfval  16188  mreacs  16300  joinfval  16982  meetfval  16996  pwsco1mhm  17351  pwsco2mhm  17352  vrmdfval  17374  galactghm  17804  symgextfv  17819  symgextfve  17820  symgfixfolem1  17839  pmtrval  17852  pmtrfv  17853  pmtrdifwrdel2lem1  17885  efgtf  18116  gsummhm2  18320  gsummpt1n0  18345  dprdfid  18397  lspval  18956  rrgsupp  19272  aspval  19309  evlslem3  19495  coe1tmfv1  19625  coe1tmfv2  19626  ply1sclid  19639  uvcval  20105  uvcvval  20106  marepvval  20354  submaval0  20367  m2detleiblem3  20416  m2detleiblem4  20417  maduval  20425  minmar1val0  20434  toponsspwpw  20707  tgval  20740  cldval  20808  ntrfval  20809  clsfval  20810  ntrval  20821  clsval  20822  opncldf2  20870  opncldf3  20871  neifval  20884  neival  20887  lpfval  20923  lpval  20924  1stcfb  21229  islocfin  21301  cnmpt11  21447  cnmpt21  21455  cnmptkp  21464  cnmptk1p  21469  kqfval  21507  stdbdxmet  22301  cmetcaulem  23067  bcth3  23109  iunmbl  23302  itg2gt0  23508  ellimc2  23622  cnmptlimc  23635  limccnp  23636  limcco  23638  coe1termlem  23995  coe1term  23996  ulmval  24115  pserulm  24157  rlimcnp  24673  xrlimcnp  24676  dchrelbasd  24945  clwlksfoclwwlk  26943  clwlksf1clwwlk  26949  grpoinvfval  27346  grpodivfval  27358  spanval  28162  nlfnval  28710  sigaval  30147  measval  30235  measdivcstOLD  30261  measdivcst  30262  probfinmeasbOLD  30464  ptpconn  31189  cvmsval  31222  climlec3  31594  bdayval  31775  madeval  31909  imageval  32012  fvimage  32013  tailfval  32342  tailval  32343  bj-diagval  33061  curfv  33360  heiborlem4  33584  heiborlem6  33586  lkrval  34194  pclvalN  34995  cdleme31fv  35497  docavalN  36231  dochval  36459  mapdval  36736  hvmapval  36868  hvmapvalvalN  36869  hdmap1vallem  36906  hdmapval  36939  hgmapval  36998  mzpval  37114  mzpsubst  37130  rabdiophlem2  37185  fphpdo  37200  monotoddzz  37327  pw2f1o2val  37425  dnnumch3lem  37435  pwssplit4  37478  hbtlem1  37512  rgspnval  37557  eliunov2  37790  fvmptiunrelexplb0d  37795  fvmptiunrelexplb1d  37797  refsum2cnlem1  39016  fmuldfeq  39615  cncfiooicclem1  39869  stoweidlem26  40006  stoweidlem30  40010  stoweidlem31  40011  stoweidlem34  40014  stirlinglem5  40058  stirlinglem8  40061  fourierdlem50  40136  sge0snmptf  40417  caragenval  40470  fargshiftfv  41139  lincvalsc0  41975  linc0scn0  41977  linc1  41979  lincscm  41984  el0ldep  42020
  Copyright terms: Public domain W3C validator