Theorem fvmptg 6947

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃*wmo 2538  {copab 5162   ↦ cmpt 5181  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  fvmpti  6948  fvmpt  6949  fvmpt2f  6950  fvtresfn  6952  fvmpts  6953  fvmpt3  6954  fvmptd3  6973  fvmptss2  6976  f1mpt  7217  bropfvvvv  8044  tz7.44-3  8349  pw2f1olem  9021  wdom2d  9497  tz9.12lem3  9713  djurcl  9835  djur  9843  djuun  9850  cardval3  9876  cfval  10169  coftr  10195  fin1a2lem1  10322  fin1a2lem12  10333  axdc2lem  10370  pwcfsdom  10506  tskmval  10762  lsw  14499  swrdswrd  14640  trclfv  14935  relexpsucnnr  14960  dfrtrclrec2  14993  rtrclreclem2  14994  summolem2a  15650  prodmolem2a  15869  divsfval  17480  joinfval  18306  meetfval  18320  symgextfv  19359  symgextfve  19360  pmtrdifwrdel2lem1  19425  efgtf  19663  rrgsupp  20646  uvcvval  21753  ply1sclid  22242  submaval0  22536  m2detleiblem3  22585  m2detleiblem4  22586  maduval  22594  minmar1val0  22603  toponsspwpw  22878  cldval  22979  ntrfval  22980  clsfval  22981  opncldf3  23042  neifval  23055  lpfval  23094  islocfin  23473  kqfval  23679  stdbdxmet  24471  cmetcaulem  25256  bcth3  25299  itg2gt0  25729  ellimc2  25846  coe1termlem  26231  bdayval  27628  oldval  27842  clwlkclwwlkfo  30096  grpoinvfval  30609  grpodivfval  30621  nlfnval  31968  sigaval  34288  measval  34375  measdivcst  34401  measdivcstALTV  34402  probfinmeasbALTV  34606  ptpconn  35446  cvmsval  35479  ex-sategoelel12  35640  imageval  36141  fvimage  36142  tailfval  36585  tailval  36586  curfv  37845  heiborlem4  38059  lkrval  39458  cdleme31fv  40760  docavalN  41493  dochval  41721  mapdval  41998  hvmapval  42130  hvmapvalvalN  42131  hdmap1vallem  42167  hdmapval  42198  hgmapval  42257  mzpval  43083  mzpsubst  43099  pw2f1o2val  43390  refsum2cnlem1  45391  stoweidlem26  46378  stirlinglem8  46433  fourierdlem50  46508  caragenval  46845  nthrucw  47238  fargshiftfv  47793  lincvalsc0  48775  linc0scn0  48777  linc1  48779  lincscm  48784