Theorem fvmptg 6531

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ∃*wmo 2603  {copab 4937   ↦ cmpt 4954  ‘cfv 6127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pr 5129

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-iota 6090  df-fun 6129  df-fv 6135

This theorem is referenced by:  fvmpti  6532  fvmpt  6533  fvmpt2f  6534  fvtresfn  6535  fvmpts  6536  fvmpt3  6537  fvmptss2  6557  f1mpt  6778  undefval  7672  tz7.44-2  7774  tz7.44-3  7775  fvdiagfn  8175  pw2f1olem  8339  fival  8593  wdom2d  8761  tz9.12lem3  8936  djulcl  9056  djurcl  9057  djur  9065  djuun  9072  cardval3  9098  cfval  9391  coftr  9417  isf34lem1  9516  fin1a2lem1  9544  fin1a2lem12  9555  axdc2lem  9592  pwcfsdom  9727  tskmval  9983  lsw  13631  swrdswrd  13791  trclfv  14125  relexpsucnnr  14149  dfrtrclrec2  14181  rtrclreclem1  14182  summolem2a  14830  prodmolem2a  15044  divsfval  16567  joinfval  17361  meetfval  17375  symgextfv  18195  symgextfve  18196  pmtrval  18228  pmtrdifwrdel2lem1  18261  efgtf  18493  rrgsupp  19659  ply1sclid  20025  uvcval  20498  uvcvval  20499  submaval0  20761  m2detleiblem3  20810  m2detleiblem4  20811  maduval  20819  minmar1val0  20828  toponsspwpw  21104  tgval  21137  cldval  21205  ntrfval  21206  clsfval  21207  opncldf2  21267  opncldf3  21268  neifval  21281  neival  21284  lpfval  21320  islocfin  21698  kqfval  21904  stdbdxmet  22697  cmetcaulem  23463  bcth3  23506  itg2gt0  23933  ellimc2  24047  coe1termlem  24420  clwlkclwwlkfoOLD  27349  clwlkclwwlkfo  27353  clwlksfoclwwlkOLD  27439  clwlksf1clwwlkOLD  27445  grpoinvfval  27928  grpodivfval  27940  nlfnval  29291  sigaval  30714  measval  30802  measdivcstOLD  30828  measdivcst  30829  probfinmeasbOLD  31032  ptpconn  31757  cvmsval  31790  bdayval  32335  imageval  32571  fvimage  32572  tailfval  32900  tailval  32901  bj-diagval  33618  curfv  33931  heiborlem4  34154  lkrval  35162  cdleme31fv  36464  docavalN  37197  dochval  37425  mapdval  37702  hvmapval  37834  hvmapvalvalN  37835  hdmap1vallem  37871  hdmapval  37902  hgmapval  37961  mzpval  38138  mzpsubst  38154  pw2f1o2val  38448  eliunov2  38811  refsum2cnlem1  40013  stoweidlem26  41035  stirlinglem8  41090  fourierdlem50  41165  caragenval  41499  fargshiftfv  42261  lincvalsc0  43075  linc0scn0  43077  linc1  43079  lincscm  43084