Theorem fvmptg 7013

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃*wmo 2535  {copab 5209   ↦ cmpt 5230  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570

This theorem is referenced by:  fvmpti  7014  fvmpt  7015  fvmpt2f  7016  fvtresfn  7017  fvmpts  7018  fvmpt3  7019  fvmptd3  7038  fvmptss2  7041  f1mpt  7280  bropfvvvv  8115  tz7.44-3  8446  pw2f1olem  9114  wdom2d  9617  tz9.12lem3  9826  djurcl  9948  djur  9956  djuun  9963  cardval3  9989  cfval  10284  coftr  10310  fin1a2lem1  10437  fin1a2lem12  10448  axdc2lem  10485  pwcfsdom  10620  tskmval  10876  lsw  14598  swrdswrd  14739  trclfv  15035  relexpsucnnr  15060  dfrtrclrec2  15093  rtrclreclem2  15094  summolem2a  15747  prodmolem2a  15966  divsfval  17593  joinfval  18430  meetfval  18444  symgextfv  19450  symgextfve  19451  pmtrdifwrdel2lem1  19516  efgtf  19754  rrgsupp  20717  uvcvval  21823  ply1sclid  22306  submaval0  22601  m2detleiblem3  22650  m2detleiblem4  22651  maduval  22659  minmar1val0  22668  toponsspwpw  22943  cldval  23046  ntrfval  23047  clsfval  23048  opncldf3  23109  neifval  23122  lpfval  23161  islocfin  23540  kqfval  23746  stdbdxmet  24543  cmetcaulem  25335  bcth3  25378  itg2gt0  25809  ellimc2  25926  coe1termlem  26311  bdayval  27707  oldval  27907  clwlkclwwlkfo  30037  grpoinvfval  30550  grpodivfval  30562  nlfnval  31909  sigaval  34091  measval  34178  measdivcst  34204  measdivcstALTV  34205  probfinmeasbALTV  34410  ptpconn  35217  cvmsval  35250  ex-sategoelel12  35411  imageval  35911  fvimage  35912  tailfval  36354  tailval  36355  curfv  37586  heiborlem4  37800  lkrval  39069  cdleme31fv  40372  docavalN  41105  dochval  41333  mapdval  41610  hvmapval  41742  hvmapvalvalN  41743  hdmap1vallem  41779  hdmapval  41810  hgmapval  41869  mzpval  42719  mzpsubst  42735  pw2f1o2val  43027  refsum2cnlem1  44974  stoweidlem26  45981  stirlinglem8  46036  fourierdlem50  46111  caragenval  46448  fargshiftfv  47363  lincvalsc0  48266  linc0scn0  48268  linc1  48270  lincscm  48275