Theorem fvmptg 6855

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 2738	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2749	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2742	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3637	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5154	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2766	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6853	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 20	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∃*wmo 2538  {copab 5132   ↦ cmpt 5153  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fvmpti  6856  fvmpt  6857  fvmpt2f  6858  fvtresfn  6859  fvmpts  6860  fvmpt3  6861  fvmptd3  6880  fvmptss2  6882  f1mpt  7115  bropfvvvv  7903  tz7.44-3  8210  pw2f1olem  8816  wdom2d  9269  tz9.12lem3  9478  djurcl  9600  djur  9608  djuun  9615  cardval3  9641  cfval  9934  coftr  9960  fin1a2lem1  10087  fin1a2lem12  10098  axdc2lem  10135  pwcfsdom  10270  tskmval  10526  lsw  14195  swrdswrd  14346  trclfv  14639  relexpsucnnr  14664  dfrtrclrec2  14697  rtrclreclem2  14698  summolem2a  15355  prodmolem2a  15572  divsfval  17175  joinfval  18006  meetfval  18020  symgextfv  18941  symgextfve  18942  pmtrdifwrdel2lem1  19007  efgtf  19243  rrgsupp  20475  uvcvval  20903  ply1sclid  21369  submaval0  21637  m2detleiblem3  21686  m2detleiblem4  21687  maduval  21695  minmar1val0  21704  toponsspwpw  21979  cldval  22082  ntrfval  22083  clsfval  22084  opncldf3  22145  neifval  22158  lpfval  22197  islocfin  22576  kqfval  22782  stdbdxmet  23577  cmetcaulem  24357  bcth3  24400  itg2gt0  24830  ellimc2  24946  coe1termlem  25324  clwlkclwwlkfo  28274  grpoinvfval  28785  grpodivfval  28797  nlfnval  30144  sigaval  31979  measval  32066  measdivcst  32092  measdivcstALTV  32093  probfinmeasbALTV  32296  ptpconn  33095  cvmsval  33128  ex-sategoelel12  33289  bdayval  33778  oldval  33965  imageval  34159  fvimage  34160  tailfval  34488  tailval  34489  curfv  35684  heiborlem4  35899  lkrval  37029  cdleme31fv  38331  docavalN  39064  dochval  39292  mapdval  39569  hvmapval  39701  hvmapvalvalN  39702  hdmap1vallem  39738  hdmapval  39769  hgmapval  39828  mzpval  40470  mzpsubst  40486  pw2f1o2val  40777  refsum2cnlem1  42469  stoweidlem26  43457  stirlinglem8  43512  fourierdlem50  43587  caragenval  43921  fargshiftfv  44779  lincvalsc0  45650  linc0scn0  45652  linc1  45654  lincscm  45659