Theorem fvmptg 6969

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃*wmo 2532  {copab 5172   ↦ cmpt 5191  ‘cfv 6514

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  fvmpti  6970  fvmpt  6971  fvmpt2f  6972  fvtresfn  6973  fvmpts  6974  fvmpt3  6975  fvmptd3  6994  fvmptss2  6997  f1mpt  7239  bropfvvvv  8074  tz7.44-3  8379  pw2f1olem  9050  wdom2d  9540  tz9.12lem3  9749  djurcl  9871  djur  9879  djuun  9886  cardval3  9912  cfval  10207  coftr  10233  fin1a2lem1  10360  fin1a2lem12  10371  axdc2lem  10408  pwcfsdom  10543  tskmval  10799  lsw  14536  swrdswrd  14677  trclfv  14973  relexpsucnnr  14998  dfrtrclrec2  15031  rtrclreclem2  15032  summolem2a  15688  prodmolem2a  15907  divsfval  17517  joinfval  18339  meetfval  18353  symgextfv  19355  symgextfve  19356  pmtrdifwrdel2lem1  19421  efgtf  19659  rrgsupp  20617  uvcvval  21702  ply1sclid  22181  submaval0  22474  m2detleiblem3  22523  m2detleiblem4  22524  maduval  22532  minmar1val0  22541  toponsspwpw  22816  cldval  22917  ntrfval  22918  clsfval  22919  opncldf3  22980  neifval  22993  lpfval  23032  islocfin  23411  kqfval  23617  stdbdxmet  24410  cmetcaulem  25195  bcth3  25238  itg2gt0  25668  ellimc2  25785  coe1termlem  26170  bdayval  27567  oldval  27769  clwlkclwwlkfo  29945  grpoinvfval  30458  grpodivfval  30470  nlfnval  31817  sigaval  34108  measval  34195  measdivcst  34221  measdivcstALTV  34222  probfinmeasbALTV  34427  ptpconn  35227  cvmsval  35260  ex-sategoelel12  35421  imageval  35925  fvimage  35926  tailfval  36367  tailval  36368  curfv  37601  heiborlem4  37815  lkrval  39088  cdleme31fv  40391  docavalN  41124  dochval  41352  mapdval  41629  hvmapval  41761  hvmapvalvalN  41762  hdmap1vallem  41798  hdmapval  41829  hgmapval  41888  mzpval  42727  mzpsubst  42743  pw2f1o2val  43035  refsum2cnlem1  45038  stoweidlem26  46031  stirlinglem8  46086  fourierdlem50  46161  caragenval  46498  fargshiftfv  47444  lincvalsc0  48414  linc0scn0  48416  linc1  48418  lincscm  48423