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

Theorem fvmptg 6189
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 2610 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2620 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2614 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3349 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4645 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2632 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6188 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  ∃*wmo 2459  {copab 4642  cmpt 4643  cfv 5804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812
This theorem is referenced by:  fvmpti  6190  fvmpt  6191  fvmpt2f  6192  fvtresfn  6193  fvmpts  6194  fvmpt3  6195  fvmptss2  6212  f1mpt  6419  undefval  7289  tz7.44-2  7390  tz7.44-3  7391  fvdiagfn  7788  resixpfo  7832  pw2f1olem  7949  fival  8201  wdom2d  8368  cantnfp1lem1  8458  cantnfp1lem2  8459  cantnfp1lem3  8460  wemapwe  8477  tz9.12lem3  8535  rankvalb  8543  cardval3  8661  cfval  8952  coftr  8978  fin23lem27  9033  isf34lem1  9077  fin1a2lem1  9105  fin1a2lem12  9116  axdc2lem  9153  pwcfsdom  9284  canthp1lem2  9354  wuncval  9443  tskmval  9540  lsw  13204  swrdswrd  13312  trclfv  13589  relexpsucnnr  13613  dfrtrclrec2  13645  rtrclreclem1  13646  climrlim2  14126  summolem3  14292  summolem2a  14293  prodmolem3  14502  prodmolem2a  14503  iprodmul  14573  iserodd  15378  divsfval  16030  mreacs  16142  joinfval  16824  meetfval  16838  pwsco1mhm  17193  pwsco2mhm  17194  vrmdfval  17216  galactghm  17646  symgextfv  17661  symgextfve  17662  symgfixfolem1  17681  pmtrval  17694  pmtrfv  17695  pmtrdifwrdel2lem1  17727  efgtf  17958  gsummhm2  18162  gsummpt1n0  18187  dprdfid  18239  lspval  18796  rrgsupp  19112  aspval  19149  evlslem3  19335  coe1tmfv1  19465  coe1tmfv2  19466  ply1sclid  19479  uvcval  19943  uvcvval  19944  marepvval  20192  submaval0  20205  m2detleiblem3  20254  m2detleiblem4  20255  maduval  20263  minmar1val0  20272  tgval  20570  cldval  20637  ntrfval  20638  clsfval  20639  ntrval  20650  clsval  20651  opncldf2  20699  opncldf3  20700  neifval  20713  neival  20716  lpfval  20752  lpval  20753  1stcfb  21058  islocfin  21130  cnmpt11  21276  cnmpt21  21284  cnmptkp  21293  cnmptk1p  21298  kqfval  21336  stdbdxmet  22130  cmetcaulem  22894  bcth3  22936  iunmbl  23128  itg2gt0  23333  ellimc2  23447  cnmptlimc  23460  limccnp  23461  limcco  23463  coe1termlem  23818  coe1term  23819  ulmval  23938  pserulm  23980  rlimcnp  24492  xrlimcnp  24495  dchrelbasd  24764  nbgraf1olem4  25973  fargshiftfv  26163  wwlkn  26210  clwwlkn  26295  clwlkfoclwwlk  26372  clwlkf1clwwlk  26377  rusgranumwlklem1  26476  usg2spot2nb  26592  usgreg2spot  26594  2spotmdisj  26595  usgreghash2spot  26596  numclwlk1lem2fv  26620  numclwlk2lem2fv  26631  grpoinvfval  26760  grpodivfval  26772  spanval  27576  nlfnval  28124  sigaval  29500  measval  29588  measdivcstOLD  29614  measdivcst  29615  probfinmeasbOLD  29817  ptpcon  30469  cvmsval  30502  climlec3  30872  bdayval  31045  imageval  31207  fvimage  31208  tailfval  31537  tailval  31538  bj-toponss  32241  bj-diagval  32267  curfv  32559  heiborlem4  32783  heiborlem6  32785  lkrval  33393  pclvalN  34194  cdleme31fv  34696  docavalN  35430  dochval  35658  mapdval  35935  hvmapval  36067  hvmapvalvalN  36068  hdmap1vallem  36105  hdmapval  36138  hgmapval  36197  mzpval  36313  mzpsubst  36329  rabdiophlem2  36384  fphpdo  36399  monotoddzz  36526  pw2f1o2val  36624  dnnumch3lem  36634  pwssplit4  36677  hbtlem1  36712  rgspnval  36757  eliunov2  36990  fvmptiunrelexplb0d  36995  fvmptiunrelexplb1d  36997  refsum2cnlem1  38219  fmuldfeq  38650  cncfiooicclem1  38779  stoweidlem26  38919  stoweidlem30  38923  stoweidlem31  38924  stoweidlem34  38927  stirlinglem5  38971  stirlinglem8  38974  fourierdlem50  39049  sge0snmptf  39330  caragenval  39383  clwlksfoclwwlk  41270  clwlksf1clwwlk  41276  fusgr2wsp2nb  41498  fusgreg2wsp  41500  lincvalsc0  42004  linc0scn0  42006  linc1  42008  lincscm  42013  el0ldep  42049
  Copyright terms: Public domain W3C validator