Theorem fvmptg 6932

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃*wmo 2531  {copab 5157   ↦ cmpt 5176  ‘cfv 6486

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmpti  6933  fvmpt  6934  fvmpt2f  6935  fvtresfn  6936  fvmpts  6937  fvmpt3  6938  fvmptd3  6957  fvmptss2  6960  f1mpt  7202  bropfvvvv  8032  tz7.44-3  8337  pw2f1olem  9005  wdom2d  9491  tz9.12lem3  9704  djurcl  9826  djur  9834  djuun  9841  cardval3  9867  cfval  10160  coftr  10186  fin1a2lem1  10313  fin1a2lem12  10324  axdc2lem  10361  pwcfsdom  10496  tskmval  10752  lsw  14489  swrdswrd  14629  trclfv  14925  relexpsucnnr  14950  dfrtrclrec2  14983  rtrclreclem2  14984  summolem2a  15640  prodmolem2a  15859  divsfval  17469  joinfval  18295  meetfval  18309  symgextfv  19315  symgextfve  19316  pmtrdifwrdel2lem1  19381  efgtf  19619  rrgsupp  20604  uvcvval  21711  ply1sclid  22190  submaval0  22483  m2detleiblem3  22532  m2detleiblem4  22533  maduval  22541  minmar1val0  22550  toponsspwpw  22825  cldval  22926  ntrfval  22927  clsfval  22928  opncldf3  22989  neifval  23002  lpfval  23041  islocfin  23420  kqfval  23626  stdbdxmet  24419  cmetcaulem  25204  bcth3  25247  itg2gt0  25677  ellimc2  25794  coe1termlem  26179  bdayval  27576  oldval  27782  clwlkclwwlkfo  29971  grpoinvfval  30484  grpodivfval  30496  nlfnval  31843  sigaval  34077  measval  34164  measdivcst  34190  measdivcstALTV  34191  probfinmeasbALTV  34396  ptpconn  35205  cvmsval  35238  ex-sategoelel12  35399  imageval  35903  fvimage  35904  tailfval  36345  tailval  36346  curfv  37579  heiborlem4  37793  lkrval  39066  cdleme31fv  40369  docavalN  41102  dochval  41330  mapdval  41607  hvmapval  41739  hvmapvalvalN  41740  hdmap1vallem  41776  hdmapval  41807  hgmapval  41866  mzpval  42705  mzpsubst  42721  pw2f1o2val  43012  refsum2cnlem1  45015  stoweidlem26  46008  stirlinglem8  46063  fourierdlem50  46138  caragenval  46475  fargshiftfv  47424  lincvalsc0  48407  linc0scn0  48409  linc1  48411  lincscm  48416