Theorem fvmptg 6969

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.

Step	Hyp	Ref	Expression
1		eqid 2761	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2772	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2765	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3669	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5181	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2784	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6967	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 20	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∃*wmo 2563  {copab 5161   ↦ cmpt 5180  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525

This theorem is referenced by:  fvmpti  6970  fvmpt  6971  fvmpt2f  6972  fvtresfn  6974  fvmpts  6975  fvmpt3  6976  fvmptd3  6995  fvmptss2  6998  f1mpt  7241  bropfvvvv  8066  tz7.44-3  8374  pw2f1olem  9049  wdom2d  9525  tz9.12lem3  9744  djurcl  9866  djur  9874  djuun  9881  cardval3  9907  cfval  10200  coftr  10227  fin1a2lem1  10354  fin1a2lem12  10365  axdc2lem  10402  pwcfsdom  10538  tskmval  10794  lsw  14574  swrdswrd  14715  trclfv  15010  relexpsucnnr  15035  dfrtrclrec2  15068  rtrclreclem2  15069  summolem2a  15725  prodmolem2a  15947  divsfval  17560  joinfval  18386  meetfval  18400  symgextfv  19441  symgextfve  19442  pmtrdifwrdel2lem1  19507  efgtf  19745  rrgsupp  20730  uvcvval  21818  ply1sclid  22331  submaval0  22620  m2detleiblem3  22669  m2detleiblem4  22670  maduval  22678  minmar1val0  22687  toponsspwpw  22962  cldval  23063  ntrfval  23064  clsfval  23065  opncldf3  23126  neifval  23139  lpfval  23178  islocfin  23557  kqfval  23763  stdbdxmet  24555  cmetcaulem  25330  bcth3  25373  itg2gt0  25802  ellimc2  25919  coe1termlem  26298  bdayval  27689  oldval  27904  clwlkclwwlkfo  30157  grpoinvfval  30671  grpodivfval  30683  nlfnval  32030  sigaval  34369  measval  34456  measdivcst  34482  measdivcstALTV  34483  probfinmeasbALTV  34687  ptpconn  35547  cvmsval  35580  ex-sategoelel12  35741  imageval  36242  fvimage  36243  tailfval  36696  tailval  36697  curfv  38063  heiborlem4  38277  lkrval  39676  cdleme31fv  40978  docavalN  41711  dochval  41939  mapdval  42216  hvmapval  42348  hvmapvalvalN  42349  hdmap1vallem  42385  hdmapval  42416  hgmapval  42475  mzpval  43277  mzpsubst  43293  pw2f1o2val  43580  refsum2cnlem1  45581  stoweidlem26  46564  stirlinglem8  46619  fourierdlem50  46694  caragenval  47031  nthrucw  47426  fargshiftfv  48009  lincvalsc0  49007  linc0scn0  49009  linc1  49011  lincscm  49016