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

Theorem fvmptg 6423
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 2771 . 2 𝐶 = 𝐶
2 fvmptg.1 . . . 4 (𝑥 = 𝐴𝐵 = 𝐶)
32eqeq2d 2781 . . 3 (𝑥 = 𝐴 → (𝑦 = 𝐵𝑦 = 𝐶))
4 eqeq1 2775 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐶𝐶 = 𝐶))
5 moeq 3535 . . . 4 ∃*𝑦 𝑦 = 𝐵
65a1i 11 . . 3 (𝑥𝐷 → ∃*𝑦 𝑦 = 𝐵)
7 fvmptg.2 . . . 4 𝐹 = (𝑥𝐷𝐵)
8 df-mpt 4865 . . . 4 (𝑥𝐷𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
97, 8eqtri 2793 . . 3 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐷𝑦 = 𝐵)}
103, 4, 6, 9fvopab3ig 6421 . 2 ((𝐴𝐷𝐶𝑅) → (𝐶 = 𝐶 → (𝐹𝐴) = 𝐶))
111, 10mpi 20 1 ((𝐴𝐷𝐶𝑅) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  ∃*wmo 2619  {copab 4847  cmpt 4864  cfv 6032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-iota 5995  df-fun 6034  df-fv 6040
This theorem is referenced by:  fvmpti  6424  fvmpt  6425  fvmpt2f  6426  fvtresfn  6427  fvmpts  6428  fvmpt3  6429  fvmptss2  6447  f1mpt  6662  undefval  7555  tz7.44-2  7657  tz7.44-3  7658  fvdiagfn  8057  resixpfo  8101  pw2f1olem  8221  fival  8475  wdom2d  8642  cantnfp1lem1  8740  cantnfp1lem2  8741  cantnfp1lem3  8742  wemapwe  8759  tz9.12lem3  8817  rankvalb  8825  djulcl  8937  djurcl  8938  djur  8946  djuun  8953  cardval3  8979  cfval  9272  coftr  9298  fin23lem27  9353  isf34lem1  9397  fin1a2lem1  9425  fin1a2lem12  9436  axdc2lem  9473  pwcfsdom  9608  canthp1lem2  9678  wuncval  9767  tskmval  9864  lsw  13549  swrdswrd  13670  trclfv  13950  relexpsucnnr  13974  dfrtrclrec2  14006  rtrclreclem1  14007  climrlim2  14487  summolem3  14654  summolem2a  14655  prodmolem3  14871  prodmolem2a  14872  iprodmul  14941  iserodd  15748  divsfval  16416  mreacs  16527  joinfval  17210  meetfval  17224  pwsco1mhm  17579  pwsco2mhm  17580  vrmdfval  17602  galactghm  18031  symgextfv  18046  symgextfve  18047  symgfixfolem1  18066  pmtrval  18079  pmtrfv  18080  pmtrdifwrdel2lem1  18112  efgtf  18343  gsummhm2  18547  gsummpt1n0  18572  dprdfid  18625  lspval  19189  rrgsupp  19507  aspval  19544  evlslem3  19730  coe1tmfv1  19860  coe1tmfv2  19861  ply1sclid  19874  uvcval  20342  uvcvval  20343  marepvval  20592  submaval0  20605  m2detleiblem3  20654  m2detleiblem4  20655  maduval  20663  minmar1val0  20672  toponsspwpw  20948  tgval  20981  cldval  21049  ntrfval  21050  clsfval  21051  ntrval  21062  clsval  21063  opncldf2  21111  opncldf3  21112  neifval  21125  neival  21128  lpfval  21164  lpval  21165  1stcfb  21470  islocfin  21542  cnmpt11  21688  cnmpt21  21696  cnmptkp  21705  cnmptk1p  21710  kqfval  21748  stdbdxmet  22541  cmetcaulem  23306  bcth3  23348  iunmbl  23542  itg2gt0  23748  ellimc2  23862  cnmptlimc  23875  limccnp  23876  limcco  23878  coe1termlem  24235  coe1term  24236  ulmval  24355  pserulm  24397  rlimcnp  24914  xrlimcnp  24917  dchrelbasd  25186  clwlkclwwlkfo  27160  clwlksfoclwwlkOLD  27245  clwlksf1clwwlkOLD  27251  grpoinvfval  27717  grpodivfval  27729  spanval  28533  nlfnval  29081  sigaval  30514  measval  30602  measdivcstOLD  30628  measdivcst  30629  probfinmeasbOLD  30831  ptpconn  31554  cvmsval  31587  climlec3  31958  bdayval  32139  madeval  32273  imageval  32375  fvimage  32376  tailfval  32705  tailval  32706  bj-diagval  33428  curfv  33723  heiborlem4  33946  heiborlem6  33948  lkrval  34898  pclvalN  35699  cdleme31fv  36200  docavalN  36934  dochval  37162  mapdval  37439  hvmapval  37571  hvmapvalvalN  37572  hdmap1vallem  37608  hdmapval  37639  hgmapval  37698  mzpval  37822  mzpsubst  37838  rabdiophlem2  37893  fphpdo  37908  monotoddzz  38035  pw2f1o2val  38133  dnnumch3lem  38143  pwssplit4  38186  hbtlem1  38220  rgspnval  38265  eliunov2  38498  fvmptiunrelexplb0d  38503  fvmptiunrelexplb1d  38505  refsum2cnlem1  39719  fmuldfeq  40334  cncfiooicclem1  40625  stoweidlem26  40761  stoweidlem30  40765  stoweidlem31  40766  stoweidlem34  40769  stirlinglem5  40813  stirlinglem8  40816  fourierdlem50  40891  sge0snmptf  41172  caragenval  41228  fargshiftfv  41904  lincvalsc0  42739  linc0scn0  42741  linc1  42743  lincscm  42748  el0ldep  42784
  Copyright terms: Public domain W3C validator