Theorem fvmptg 6983

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃*wmo 2537  {copab 5181   ↦ cmpt 5201  ‘cfv 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538

This theorem is referenced by:  fvmpti  6984  fvmpt  6985  fvmpt2f  6986  fvtresfn  6987  fvmpts  6988  fvmpt3  6989  fvmptd3  7008  fvmptss2  7011  f1mpt  7253  bropfvvvv  8089  tz7.44-3  8420  pw2f1olem  9088  wdom2d  9592  tz9.12lem3  9801  djurcl  9923  djur  9931  djuun  9938  cardval3  9964  cfval  10259  coftr  10285  fin1a2lem1  10412  fin1a2lem12  10423  axdc2lem  10460  pwcfsdom  10595  tskmval  10851  lsw  14580  swrdswrd  14721  trclfv  15017  relexpsucnnr  15042  dfrtrclrec2  15075  rtrclreclem2  15076  summolem2a  15729  prodmolem2a  15948  divsfval  17559  joinfval  18381  meetfval  18395  symgextfv  19397  symgextfve  19398  pmtrdifwrdel2lem1  19463  efgtf  19701  rrgsupp  20659  uvcvval  21744  ply1sclid  22223  submaval0  22516  m2detleiblem3  22565  m2detleiblem4  22566  maduval  22574  minmar1val0  22583  toponsspwpw  22858  cldval  22959  ntrfval  22960  clsfval  22961  opncldf3  23022  neifval  23035  lpfval  23074  islocfin  23453  kqfval  23659  stdbdxmet  24452  cmetcaulem  25238  bcth3  25281  itg2gt0  25711  ellimc2  25828  coe1termlem  26213  bdayval  27610  oldval  27810  clwlkclwwlkfo  29936  grpoinvfval  30449  grpodivfval  30461  nlfnval  31808  sigaval  34088  measval  34175  measdivcst  34201  measdivcstALTV  34202  probfinmeasbALTV  34407  ptpconn  35201  cvmsval  35234  ex-sategoelel12  35395  imageval  35894  fvimage  35895  tailfval  36336  tailval  36337  curfv  37570  heiborlem4  37784  lkrval  39052  cdleme31fv  40355  docavalN  41088  dochval  41316  mapdval  41593  hvmapval  41725  hvmapvalvalN  41726  hdmap1vallem  41762  hdmapval  41793  hgmapval  41852  mzpval  42702  mzpsubst  42718  pw2f1o2val  43010  refsum2cnlem1  45009  stoweidlem26  46003  stirlinglem8  46058  fourierdlem50  46133  caragenval  46470  fargshiftfv  47401  lincvalsc0  48345  linc0scn0  48347  linc1  48349  lincscm  48354