Theorem fvmptg 6940

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃*wmo 2541  {copab 5141   ↦ cmpt 5160  ‘cfv 6492

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmpti  6941  fvmpt  6942  fvmpt2f  6943  fvtresfn  6945  fvmpts  6946  fvmpt3  6947  fvmptd3  6966  fvmptss2  6969  f1mpt  7212  bropfvvvv  8038  tz7.44-3  8344  pw2f1olem  9016  wdom2d  9492  tz9.12lem3  9711  djurcl  9833  djur  9841  djuun  9848  cardval3  9874  cfval  10167  coftr  10193  fin1a2lem1  10320  fin1a2lem12  10331  axdc2lem  10368  pwcfsdom  10504  tskmval  10760  lsw  14524  swrdswrd  14665  trclfv  14960  relexpsucnnr  14985  dfrtrclrec2  15018  rtrclreclem2  15019  summolem2a  15675  prodmolem2a  15897  divsfval  17509  joinfval  18335  meetfval  18349  symgextfv  19391  symgextfve  19392  pmtrdifwrdel2lem1  19457  efgtf  19695  rrgsupp  20680  uvcvval  21768  ply1sclid  22281  submaval0  22570  m2detleiblem3  22619  m2detleiblem4  22620  maduval  22628  minmar1val0  22637  toponsspwpw  22912  cldval  23013  ntrfval  23014  clsfval  23015  opncldf3  23076  neifval  23089  lpfval  23128  islocfin  23507  kqfval  23713  stdbdxmet  24505  cmetcaulem  25280  bcth3  25323  itg2gt0  25752  ellimc2  25869  coe1termlem  26248  bdayval  27637  oldval  27851  clwlkclwwlkfo  30104  grpoinvfval  30618  grpodivfval  30630  nlfnval  31977  sigaval  34302  measval  34389  measdivcst  34415  measdivcstALTV  34416  probfinmeasbALTV  34620  ptpconn  35468  cvmsval  35501  ex-sategoelel12  35662  imageval  36163  fvimage  36164  tailfval  36607  tailval  36608  curfv  37974  heiborlem4  38188  lkrval  39587  cdleme31fv  40889  docavalN  41622  dochval  41850  mapdval  42127  hvmapval  42259  hvmapvalvalN  42260  hdmap1vallem  42296  hdmapval  42327  hgmapval  42386  mzpval  43188  mzpsubst  43204  pw2f1o2val  43491  refsum2cnlem1  45492  stoweidlem26  46476  stirlinglem8  46531  fourierdlem50  46606  caragenval  46943  nthrucw  47338  fargshiftfv  47921  lincvalsc0  48919  linc0scn0  48921  linc1  48923  lincscm  48928