Theorem fvmptg 6927

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃*wmo 2533  {copab 5153   ↦ cmpt 5172  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  fvmpti  6928  fvmpt  6929  fvmpt2f  6930  fvtresfn  6931  fvmpts  6932  fvmpt3  6933  fvmptd3  6952  fvmptss2  6955  f1mpt  7195  bropfvvvv  8022  tz7.44-3  8327  pw2f1olem  8994  wdom2d  9466  tz9.12lem3  9679  djurcl  9801  djur  9809  djuun  9816  cardval3  9842  cfval  10135  coftr  10161  fin1a2lem1  10288  fin1a2lem12  10299  axdc2lem  10336  pwcfsdom  10471  tskmval  10727  lsw  14468  swrdswrd  14609  trclfv  14904  relexpsucnnr  14929  dfrtrclrec2  14962  rtrclreclem2  14963  summolem2a  15619  prodmolem2a  15838  divsfval  17448  joinfval  18274  meetfval  18288  symgextfv  19328  symgextfve  19329  pmtrdifwrdel2lem1  19394  efgtf  19632  rrgsupp  20614  uvcvval  21721  ply1sclid  22200  submaval0  22493  m2detleiblem3  22542  m2detleiblem4  22543  maduval  22551  minmar1val0  22560  toponsspwpw  22835  cldval  22936  ntrfval  22937  clsfval  22938  opncldf3  22999  neifval  23012  lpfval  23051  islocfin  23430  kqfval  23636  stdbdxmet  24428  cmetcaulem  25213  bcth3  25256  itg2gt0  25686  ellimc2  25803  coe1termlem  26188  bdayval  27585  oldval  27793  clwlkclwwlkfo  29984  grpoinvfval  30497  grpodivfval  30509  nlfnval  31856  sigaval  34119  measval  34206  measdivcst  34232  measdivcstALTV  34233  probfinmeasbALTV  34437  ptpconn  35265  cvmsval  35298  ex-sategoelel12  35459  imageval  35963  fvimage  35964  tailfval  36405  tailval  36406  curfv  37639  heiborlem4  37853  lkrval  39126  cdleme31fv  40428  docavalN  41161  dochval  41389  mapdval  41666  hvmapval  41798  hvmapvalvalN  41799  hdmap1vallem  41835  hdmapval  41866  hgmapval  41925  mzpval  42764  mzpsubst  42780  pw2f1o2val  43071  refsum2cnlem1  45073  stoweidlem26  46063  stirlinglem8  46118  fourierdlem50  46193  caragenval  46530  fargshiftfv  47469  lincvalsc0  48452  linc0scn0  48454  linc1  48456  lincscm  48461