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

Theorem fvmptg 6078
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 2514 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2524 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2518 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3253 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4543 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2536 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6077 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1938  ∃*wmo 2363  {copab 4540  cmpt 4541  cfv 5694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
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 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-iota 5658  df-fun 5696  df-fv 5702
This theorem is referenced by:  fvmpti  6079  fvmpt  6080  fvmpt2f  6081  fvtresfn  6082  fvmpts  6083  fvmpt3  6084  fvmptss2  6101  f1mpt  6301  undefval  7169  tz7.44-2  7270  tz7.44-3  7271  fvdiagfn  7668  resixpfo  7712  pw2f1olem  7829  fival  8081  wdom2d  8248  cantnfp1lem1  8338  cantnfp1lem2  8339  cantnfp1lem3  8340  wemapwe  8357  tz9.12lem3  8415  rankvalb  8423  cardval3  8541  cfval  8832  coftr  8858  fin23lem27  8913  isf34lem1  8957  fin1a2lem1  8985  fin1a2lem12  8996  axdc2lem  9033  pwcfsdom  9164  canthp1lem2  9234  wuncval  9323  tskmval  9420  lsw  13067  swrdswrd  13175  trclfv  13452  relexpsucnnr  13476  dfrtrclrec2  13508  rtrclreclem1  13509  climrlim2  13996  summolem3  14165  summolem2a  14166  prodmolem3  14375  prodmolem2a  14376  iprodmul  14446  iserodd  15266  divsfval  15926  mreacs  16038  joinfval  16720  meetfval  16734  pwsco1mhm  17089  pwsco2mhm  17090  vrmdfval  17112  galactghm  17542  symgextfv  17557  symgextfve  17558  symgfixfolem1  17577  pmtrval  17590  pmtrfv  17591  pmtrdifwrdel2lem1  17623  efgtf  17870  gsummhm2  18073  gsummpt1n0  18098  dprdfid  18150  lspval  18704  rrgsupp  19020  aspval  19057  evlslem3  19243  coe1tmfv1  19373  coe1tmfv2  19374  ply1sclid  19387  uvcval  19850  uvcvval  19851  marepvval  20099  submaval0  20112  m2detleiblem3  20161  m2detleiblem4  20162  maduval  20170  minmar1val0  20179  tgval  20477  cldval  20544  ntrfval  20545  clsfval  20546  ntrval  20557  clsval  20558  opncldf2  20606  opncldf3  20607  neifval  20620  neival  20623  lpfval  20659  lpval  20660  1stcfb  20965  islocfin  21037  cnmpt11  21183  cnmpt21  21191  cnmptkp  21200  cnmptk1p  21205  kqfval  21243  stdbdxmet  22036  cmetcaulem  22762  bcth3  22803  iunmbl  23007  itg2gt0  23212  ellimc2  23326  cnmptlimc  23339  limccnp  23340  limcco  23342  coe1termlem  23706  coe1term  23707  ulmval  23829  pserulm  23871  rlimcnp  24383  xrlimcnp  24386  dchrelbasd  24657  nbgraf1olem4  25715  fargshiftfv  25905  wwlkn  25952  clwwlkn  26037  clwlkfoclwwlk  26114  clwlkf1clwwlk  26119  rusgranumwlklem1  26218  usg2spot2nb  26334  usgreg2spot  26336  2spotmdisj  26337  usgreghash2spot  26338  numclwlk1lem2fv  26362  numclwlk2lem2fv  26373  grpoinvfval  26502  grpodivfval  26514  spanval  27368  nlfnval  27916  sigaval  29300  measval  29388  measdivcstOLD  29414  measdivcst  29415  probfinmeasbOLD  29628  ptpcon  30318  cvmsval  30351  climlec3  30718  bdayval  30884  imageval  31046  fvimage  31047  tailfval  31375  tailval  31376  bj-toponss  32076  bj-diagval  32102  curfv  32453  heiborlem4  32677  heiborlem6  32679  lkrval  33287  pclvalN  34088  cdleme31fv  34590  docavalN  35324  dochval  35552  mapdval  35829  hvmapval  35961  hvmapvalvalN  35962  hdmap1vallem  35999  hdmapval  36032  hgmapval  36091  mzpval  36207  mzpsubst  36223  rabdiophlem2  36278  fphpdo  36293  monotoddzz  36420  pw2f1o2val  36518  dnnumch3lem  36528  pwssplit4  36571  hbtlem1  36606  rgspnval  36658  eliunov2  36891  fvmptiunrelexplb0d  36896  fvmptiunrelexplb1d  36898  refsum2cnlem1  38120  fmuldfeq  38553  cncfiooicclem1  38683  stoweidlem26  38826  stoweidlem30  38830  stoweidlem31  38831  stoweidlem34  38834  stirlinglem5  38878  stirlinglem8  38881  fourierdlem50  38958  sge0snmptf  39241  caragenval  39294  clwlksfoclwwlk  41379  clwlksf1clwwlk  41385  fusgr2wsp2nb  41607  fusgreg2wsp  41609  lincvalsc0  42113  linc0scn0  42115  linc1  42117  lincscm  42122  el0ldep  42158
  Copyright terms: Public domain W3C validator