Theorem fvmptg 7014

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃*wmo 2538  {copab 5205   ↦ cmpt 5225  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  fvmpti  7015  fvmpt  7016  fvmpt2f  7017  fvtresfn  7018  fvmpts  7019  fvmpt3  7020  fvmptd3  7039  fvmptss2  7042  f1mpt  7281  bropfvvvv  8117  tz7.44-3  8448  pw2f1olem  9116  wdom2d  9620  tz9.12lem3  9829  djurcl  9951  djur  9959  djuun  9966  cardval3  9992  cfval  10287  coftr  10313  fin1a2lem1  10440  fin1a2lem12  10451  axdc2lem  10488  pwcfsdom  10623  tskmval  10879  lsw  14602  swrdswrd  14743  trclfv  15039  relexpsucnnr  15064  dfrtrclrec2  15097  rtrclreclem2  15098  summolem2a  15751  prodmolem2a  15970  divsfval  17592  joinfval  18418  meetfval  18432  symgextfv  19436  symgextfve  19437  pmtrdifwrdel2lem1  19502  efgtf  19740  rrgsupp  20701  uvcvval  21806  ply1sclid  22291  submaval0  22586  m2detleiblem3  22635  m2detleiblem4  22636  maduval  22644  minmar1val0  22653  toponsspwpw  22928  cldval  23031  ntrfval  23032  clsfval  23033  opncldf3  23094  neifval  23107  lpfval  23146  islocfin  23525  kqfval  23731  stdbdxmet  24528  cmetcaulem  25322  bcth3  25365  itg2gt0  25795  ellimc2  25912  coe1termlem  26297  bdayval  27693  oldval  27893  clwlkclwwlkfo  30028  grpoinvfval  30541  grpodivfval  30553  nlfnval  31900  sigaval  34112  measval  34199  measdivcst  34225  measdivcstALTV  34226  probfinmeasbALTV  34431  ptpconn  35238  cvmsval  35271  ex-sategoelel12  35432  imageval  35931  fvimage  35932  tailfval  36373  tailval  36374  curfv  37607  heiborlem4  37821  lkrval  39089  cdleme31fv  40392  docavalN  41125  dochval  41353  mapdval  41630  hvmapval  41762  hvmapvalvalN  41763  hdmap1vallem  41799  hdmapval  41830  hgmapval  41889  mzpval  42743  mzpsubst  42759  pw2f1o2val  43051  refsum2cnlem1  45042  stoweidlem26  46041  stirlinglem8  46096  fourierdlem50  46171  caragenval  46508  fargshiftfv  47426  lincvalsc0  48338  linc0scn0  48340  linc1  48342  lincscm  48347