Theorem fvmptg 6774

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 3607	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5112	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2761	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6772	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 20	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542   ∈ wcel 2113  ∃*wmo 2538  {copab 5093   ↦ cmpt 5111  ‘cfv 6340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5168  ax-nul 5175  ax-pr 5297

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-v 3400  df-sbc 3683  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-iota 6298  df-fun 6342  df-fv 6348

This theorem is referenced by:  fvmpti  6775  fvmpt  6776  fvmpt2f  6777  fvtresfn  6778  fvmpts  6779  fvmpt3  6780  fvmptd3  6799  fvmptss2  6801  f1mpt  7031  bropfvvvv  7814  tz7.44-3  8074  pw2f1olem  8671  wdom2d  9118  tz9.12lem3  9292  djurcl  9414  djur  9422  djuun  9429  cardval3  9455  cfval  9748  coftr  9774  fin1a2lem1  9901  fin1a2lem12  9912  axdc2lem  9949  pwcfsdom  10084  tskmval  10340  lsw  14006  swrdswrd  14157  trclfv  14450  relexpsucnnr  14475  dfrtrclrec2  14508  rtrclreclem2  14509  summolem2a  15166  prodmolem2a  15381  divsfval  16924  joinfval  17728  meetfval  17742  symgextfv  18665  symgextfve  18666  pmtrdifwrdel2lem1  18731  efgtf  18967  rrgsupp  20184  uvcvval  20603  ply1sclid  21064  submaval0  21332  m2detleiblem3  21381  m2detleiblem4  21382  maduval  21390  minmar1val0  21399  toponsspwpw  21674  cldval  21775  ntrfval  21776  clsfval  21777  opncldf3  21838  neifval  21851  lpfval  21890  islocfin  22269  kqfval  22475  stdbdxmet  23269  cmetcaulem  24041  bcth3  24084  itg2gt0  24513  ellimc2  24629  coe1termlem  25007  clwlkclwwlkfo  27946  grpoinvfval  28457  grpodivfval  28469  nlfnval  29816  sigaval  31649  measval  31736  measdivcst  31762  measdivcstALTV  31763  probfinmeasbALTV  31966  ptpconn  32766  cvmsval  32799  ex-sategoelel12  32960  bdayval  33492  oldval  33679  imageval  33870  fvimage  33871  tailfval  34199  tailval  34200  curfv  35377  heiborlem4  35592  lkrval  36722  cdleme31fv  38024  docavalN  38757  dochval  38985  mapdval  39262  hvmapval  39394  hvmapvalvalN  39395  hdmap1vallem  39431  hdmapval  39462  hgmapval  39521  mzpval  40118  mzpsubst  40134  pw2f1o2val  40425  refsum2cnlem1  42110  stoweidlem26  43101  stirlinglem8  43156  fourierdlem50  43231  caragenval  43565  fargshiftfv  44417  lincvalsc0  45288  linc0scn0  45290  linc1  45292  lincscm  45297