Theorem fvmptg 6983

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 2761	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2772	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2765	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3665	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5187	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2784	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6981	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 21	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃*wmo 2563  {copab 5167   ↦ cmpt 5186  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539

This theorem is used by:  fvmpti  6984  fvmpt  6985  fvmpt2f  6986  fvtresfn  6988  fvmpts  6989  fvmpt3  6990  fvmptd3  7009  fvmptss2  7012  f1mpt  7257  bropfvvvv  8092  tz7.44-3  8400  curfv  8876  pw2f1olem  9084  wdom2d  9558  tz9.12lem3  9779  djurcl  9973  djur  9981  djuun  9988  cardval3  10014  cfval  10305  coftr  10332  fin1a2lem1  10459  fin1a2lem12  10470  axdc2lem  10507  pwcfsdom  10649  tskmval  10905  lsw  14689  swrdswrd  14834  trclfv  15133  relexpsucnnr  15158  dfrtrclrec2  15191  rtrclreclem2  15192  summolem2a  15861  prodmolem2a  16081  divsfval  17699  joinfval  18525  meetfval  18539  symgextfv  19612  symgextfve  19613  pmtrdifwrdel2lem1  19678  efgtf  19916  rrgsupp  20933  uvcvval  22072  ply1sclid  22587  submaval0  22875  m2detleiblem3  22924  m2detleiblem4  22925  maduval  22933  minmar1val0  22942  toponsspwpw  23220  cldval  23321  ntrfval  23322  clsfval  23323  opncldf3  23384  neifval  23397  lpfval  23436  islocfin  23816  kqfval  24022  stdbdxmet  24814  cmetcaulem  25589  bcth3  25632  itg2gt0  26061  ellimc2  26177  coe1termlem  26557  bdayval  27987  oldval  28202  clwlkclwwlkfo  30582  grpoinvfval  31106  grpodivfval  31118  nlfnval  32465  sigaval  34725  measval  34813  measdivcst  34839  measdivcstALTV  34840  probfinmeasbALTV  35044  ptpconn  35967  cvmsval  36000  ex-sategoelel12  36161  imageval  36662  fvimage  36663  tailfval  37130  tailval  37131  heiborlem4  38716  lkrval  40113  cdleme31fv  41415  docavalN  42148  dochval  42376  mapdval  42653  hvmapval  42785  hvmapvalvalN  42786  hdmap1vallem  42822  hdmapval  42853  hgmapval  42912  mzpval  43696  mzpsubst  43712  pw2f1o2val  43999  refsum2cnlem1  45997  stoweidlem26  46980  stirlinglem8  47035  fourierdlem50  47110  caragenval  47447  fargshiftfv  48465  lincvalsc0  49477  linc0scn0  49479  linc1  49481  lincscm  49486