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

Theorem fvmptg 6013
 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 2505 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2515 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2509 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3238 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4495 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2527 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6012 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 378   = wceq 1468   ∈ wcel 1937  ∃*wmo 2354  {copab 4492   ↦ cmpt 4493  ‘cfv 5633 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680 This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-mpt 4495  df-id 4795  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-iota 5597  df-fun 5635  df-fv 5641 This theorem is referenced by:  fvmpti  6014  fvmpt  6015  fvmpt2f  6016  fvtresfn  6017  fvmpts  6018  fvmpt3  6019  fvmptss2  6036  f1mpt  6233  undefval  7100  tz7.44-2  7202  tz7.44-3  7203  fvdiagfn  7599  resixpfo  7643  pw2f1olem  7760  fival  8011  wdom2d  8178  cantnfp1lem1  8268  cantnfp1lem2  8269  cantnfp1lem3  8270  wemapwe  8287  tz9.12lem3  8345  rankvalb  8353  cardval3  8471  cfval  8762  coftr  8788  fin23lem27  8843  isf34lem1  8887  fin1a2lem1  8915  fin1a2lem12  8926  axdc2lem  8963  pwcfsdom  9093  canthp1lem2  9163  wuncval  9252  tskmval  9349  lsw  12843  swrdswrd  12950  trclfv  13224  relexpsucnnr  13248  dfrtrclrec2  13280  rtrclreclem1  13281  climrlim2  13771  summolem3  13940  summolem2a  13941  prodmolem3  14147  prodmolem2a  14148  iprodmul  14216  iserodd  14947  divsfval  15618  mreacs  15730  joinfval  16412  meetfval  16426  pwsco1mhm  16777  pwsco2mhm  16778  vrmdfval  16800  galactghm  17205  symgextfv  17220  symgextfve  17221  symgfixfolem1  17240  pmtrval  17253  pmtrfv  17254  pmtrdifwrdel2lem1  17286  efgtf  17533  gsummhm2  17733  gsummpt1n0  17758  dprdfid  17810  lspval  18358  rrgsupp  18674  aspval  18711  evlslem3  18896  coe1tmfv1  19026  coe1tmfv2  19027  ply1sclid  19040  uvcval  19501  uvcvval  19502  marepvval  19750  submaval0  19763  m2detleiblem3  19812  m2detleiblem4  19813  maduval  19821  minmar1val0  19830  tgval  20128  cldval  20195  ntrfval  20196  clsfval  20197  ntrval  20208  clsval  20209  opncldf2  20258  opncldf3  20259  neifval  20272  neival  20275  lpfval  20311  lpval  20312  1stcfb  20617  islocfin  20689  cnmpt11  20835  cnmpt21  20843  cnmptkp  20852  cnmptk1p  20857  kqfval  20895  stdbdxmet  21688  cmetcaulem  22417  bcth3  22458  iunmbl  22666  itg2gt0  22879  ellimc2  22993  cnmptlimc  23006  limccnp  23007  limcco  23009  coe1termlem  23373  coe1term  23374  ulmval  23496  pserulm  23538  rlimcnp  24052  xrlimcnp  24055  dchrelbasd  24328  nbgraf1olem4  25333  fargshiftfv  25524  wwlkn  25571  clwwlkn  25656  clwlkfoclwwlk  25733  clwlkf1clwwlk  25738  rusgranumwlklem1  25837  usg2spot2nb  25953  usgreg2spot  25955  2spotmdisj  25956  usgreghash2spot  25957  numclwlk1lem2fv  25981  numclwlk2lem2fv  25992  grpoinvfval  26115  grpodivfval  26133  gxfval  26148  issubgo  26194  spanval  27149  nlfnval  27697  sigaval  29087  measval  29175  measdivcstOLD  29201  measdivcst  29202  probfinmeasbOLD  29415  ptpcon  30108  cvmsval  30141  climlec3  30520  bdayval  30686  imageval  30848  fvimage  30849  tailfval  31177  tailval  31178  bj-toponss  31840  bj-diagval  31866  curfv  32158  heiborlem4  32383  heiborlem6  32385  lkrval  32894  pclvalN  33695  cdleme31fv  34197  docavalN  34931  dochval  35159  mapdval  35436  hvmapval  35568  hvmapvalvalN  35569  hdmap1vallem  35606  hdmapval  35639  hgmapval  35698  mzpval  35814  mzpsubst  35830  rabdiophlem2  35885  fphpdo  35900  monotoddzz  36031  pw2f1o2val  36134  dnnumch3lem  36144  pwssplit4  36187  hbtlem1  36222  rgspnval  36274  eliunov2  36510  fvmptiunrelexplb0d  36515  fvmptiunrelexplb1d  36517  refsum2cnlem1  37706  fmuldfeq  38063  cncfiooicclem1  38180  stoweidlem26  38322  stoweidlem30  38327  stoweidlem31  38328  stoweidlem34  38331  stirlinglem5  38376  stirlinglem8  38379  fourierdlem50  38456  sge0snmptf  38725  caragenval  38778  clwlksfoclwwlk  40670  clwlksf1clwwlk  40676  fusgr2wsp2nb  40898  fusgreg2wsp  40900  lincvalsc0  41404  linc0scn0  41406  linc1  41408  lincscm  41413  el0ldep  41449
 Copyright terms: Public domain W3C validator