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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃*wmo 2565  {copab 5170   ↦ cmpt 5189  ‘cfv 6558

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566

This theorem is used by:  fvmpti  7015  fvmpt  7016  fvmpt2f  7017  fvtresfn  7019  fvmpts  7020  fvmpt3  7021  fvmptd3  7040  fvmptss2  7043  f1mpt  7288  bropfvvvv  8128  tz7.44-3  8444  curfv  8920  pw2f1olem  9128  wdom2d  9601  tz9.12lem3  9823  djurcl  10019  djur  10027  djuun  10034  cardval3  10060  cfval  10351  coftr  10378  fin1a2lem1  10505  fin1a2lem12  10516  axdc2lem  10553  pwcfsdom  10695  tskmval  10951  lsw  14736  swrdswrd  14882  trclfv  15182  relexpsucnnr  15207  dfrtrclrec2  15240  rtrclreclem2  15241  summolem2a  15910  prodmolem2a  16130  divsfval  17748  joinfval  18574  meetfval  18588  symgextfv  19662  symgextfve  19663  pmtrdifwrdel2lem1  19728  efgtf  19966  rrgsupp  20983  uvcvval  22122  ply1sclid  22637  submaval0  22925  m2detleiblem3  22974  m2detleiblem4  22975  maduval  22983  minmar1val0  22992  toponsspwpw  23270  cldval  23371  ntrfval  23372  clsfval  23373  opncldf3  23434  neifval  23447  lpfval  23486  islocfin  23866  kqfval  24072  stdbdxmet  24864  cmetcaulem  25639  bcth3  25682  itg2gt0  26111  ellimc2  26227  coe1termlem  26607  bdayval  28035  oldval  28250  clwlkclwwlkfo  30630  grpoinvfval  31154  grpodivfval  31166  nlfnval  32513  sigaval  34813  measval  34901  measdivcst  34927  measdivcstALTV  34928  probfinmeasbALTV  35131  ptpconn  36165  cvmsval  36198  ex-sategoelel12  36359  mirimanoffr  36627  imageval  36870  fvimage  36871  tailfval  37338  tailval  37339  heiborlem4  38940  lkrval  40337  cdleme31fv  41639  docavalN  42372  dochval  42600  mapdval  42877  hvmapval  43009  hvmapvalvalN  43010  hdmap1vallem  43046  hdmapval  43077  hgmapval  43136  mzpval  43936  mzpsubst  43952  pw2f1o2val  44239  refsum2cnlem1  46259  stoweidlem26  47241  stirlinglem8  47296  fourierdlem50  47371  caragenval  47708  fargshiftfv  48726  lincvalsc0  49738  linc0scn0  49740  linc1  49742  lincscm  49747