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

Theorem fvmptg 6430
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 2748 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2758 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2752 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3511 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4870 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2770 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6428 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1620  wcel 2127  ∃*wmo 2596  {copab 4852  cmpt 4869  cfv 6037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-iota 6000  df-fun 6039  df-fv 6045
This theorem is referenced by:  fvmpti  6431  fvmpt  6432  fvmpt2f  6433  fvtresfn  6434  fvmpts  6435  fvmpt3  6436  fvmptss2  6454  f1mpt  6669  undefval  7559  tz7.44-2  7660  tz7.44-3  7661  fvdiagfn  8056  resixpfo  8100  pw2f1olem  8217  fival  8471  wdom2d  8638  cantnfp1lem1  8736  cantnfp1lem2  8737  cantnfp1lem3  8738  wemapwe  8755  tz9.12lem3  8813  rankvalb  8821  cardval3  8939  cfval  9232  coftr  9258  fin23lem27  9313  isf34lem1  9357  fin1a2lem1  9385  fin1a2lem12  9396  axdc2lem  9433  pwcfsdom  9568  canthp1lem2  9638  wuncval  9727  tskmval  9824  lsw  13509  swrdswrd  13631  trclfv  13911  relexpsucnnr  13935  dfrtrclrec2  13967  rtrclreclem1  13968  climrlim2  14448  summolem3  14615  summolem2a  14616  prodmolem3  14833  prodmolem2a  14834  iprodmul  14904  iserodd  15713  divsfval  16380  mreacs  16491  joinfval  17173  meetfval  17187  pwsco1mhm  17542  pwsco2mhm  17543  vrmdfval  17565  galactghm  17994  symgextfv  18009  symgextfve  18010  symgfixfolem1  18029  pmtrval  18042  pmtrfv  18043  pmtrdifwrdel2lem1  18075  efgtf  18306  gsummhm2  18510  gsummpt1n0  18535  dprdfid  18587  lspval  19148  rrgsupp  19464  aspval  19501  evlslem3  19687  coe1tmfv1  19817  coe1tmfv2  19818  ply1sclid  19831  uvcval  20297  uvcvval  20298  marepvval  20546  submaval0  20559  m2detleiblem3  20608  m2detleiblem4  20609  maduval  20617  minmar1val0  20626  toponsspwpw  20899  tgval  20932  cldval  21000  ntrfval  21001  clsfval  21002  ntrval  21013  clsval  21014  opncldf2  21062  opncldf3  21063  neifval  21076  neival  21079  lpfval  21115  lpval  21116  1stcfb  21421  islocfin  21493  cnmpt11  21639  cnmpt21  21647  cnmptkp  21656  cnmptk1p  21661  kqfval  21699  stdbdxmet  22492  cmetcaulem  23257  bcth3  23299  iunmbl  23492  itg2gt0  23697  ellimc2  23811  cnmptlimc  23824  limccnp  23825  limcco  23827  coe1termlem  24184  coe1term  24185  ulmval  24304  pserulm  24346  rlimcnp  24862  xrlimcnp  24865  dchrelbasd  25134  clwlkclwwlkfo  27103  clwlksfoclwwlkOLD  27188  clwlksf1clwwlkOLD  27194  grpoinvfval  27656  grpodivfval  27668  spanval  28472  nlfnval  29020  sigaval  30453  measval  30541  measdivcstOLD  30567  measdivcst  30568  probfinmeasbOLD  30770  ptpconn  31493  cvmsval  31526  climlec3  31897  bdayval  32078  madeval  32212  imageval  32314  fvimage  32315  tailfval  32644  tailval  32645  bj-diagval  33372  curfv  33671  heiborlem4  33895  heiborlem6  33897  lkrval  34847  pclvalN  35648  cdleme31fv  36149  docavalN  36883  dochval  37111  mapdval  37388  hvmapval  37520  hvmapvalvalN  37521  hdmap1vallem  37558  hdmapval  37591  hgmapval  37650  mzpval  37766  mzpsubst  37782  rabdiophlem2  37837  fphpdo  37852  monotoddzz  37979  pw2f1o2val  38077  dnnumch3lem  38087  pwssplit4  38130  hbtlem1  38164  rgspnval  38209  eliunov2  38442  fvmptiunrelexplb0d  38447  fvmptiunrelexplb1d  38449  refsum2cnlem1  39664  fmuldfeq  40287  cncfiooicclem1  40578  stoweidlem26  40715  stoweidlem30  40719  stoweidlem31  40720  stoweidlem34  40723  stirlinglem5  40767  stirlinglem8  40770  fourierdlem50  40845  sge0snmptf  41126  caragenval  41182  fargshiftfv  41854  lincvalsc0  42689  linc0scn0  42691  linc1  42693  lincscm  42698  el0ldep  42734
  Copyright terms: Public domain W3C validator