Theorem fvmptg 6882

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∃*wmo 2539  {copab 5137   ↦ cmpt 5158  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445

This theorem is referenced by:  fvmpti  6883  fvmpt  6884  fvmpt2f  6885  fvtresfn  6886  fvmpts  6887  fvmpt3  6888  fvmptd3  6907  fvmptss2  6909  f1mpt  7143  bropfvvvv  7941  tz7.44-3  8248  pw2f1olem  8872  wdom2d  9348  tz9.12lem3  9556  djurcl  9678  djur  9686  djuun  9693  cardval3  9719  cfval  10012  coftr  10038  fin1a2lem1  10165  fin1a2lem12  10176  axdc2lem  10213  pwcfsdom  10348  tskmval  10604  lsw  14276  swrdswrd  14427  trclfv  14720  relexpsucnnr  14745  dfrtrclrec2  14778  rtrclreclem2  14779  summolem2a  15436  prodmolem2a  15653  divsfval  17267  joinfval  18100  meetfval  18114  symgextfv  19035  symgextfve  19036  pmtrdifwrdel2lem1  19101  efgtf  19337  rrgsupp  20571  uvcvval  21002  ply1sclid  21468  submaval0  21738  m2detleiblem3  21787  m2detleiblem4  21788  maduval  21796  minmar1val0  21805  toponsspwpw  22080  cldval  22183  ntrfval  22184  clsfval  22185  opncldf3  22246  neifval  22259  lpfval  22298  islocfin  22677  kqfval  22883  stdbdxmet  23680  cmetcaulem  24461  bcth3  24504  itg2gt0  24934  ellimc2  25050  coe1termlem  25428  clwlkclwwlkfo  28382  grpoinvfval  28893  grpodivfval  28905  nlfnval  30252  sigaval  32088  measval  32175  measdivcst  32201  measdivcstALTV  32202  probfinmeasbALTV  32405  ptpconn  33204  cvmsval  33237  ex-sategoelel12  33398  bdayval  33860  oldval  34047  imageval  34241  fvimage  34242  tailfval  34570  tailval  34571  curfv  35766  heiborlem4  35981  lkrval  37109  cdleme31fv  38411  docavalN  39144  dochval  39372  mapdval  39649  hvmapval  39781  hvmapvalvalN  39782  hdmap1vallem  39818  hdmapval  39849  hgmapval  39908  mzpval  40561  mzpsubst  40577  pw2f1o2val  40868  refsum2cnlem1  42587  stoweidlem26  43574  stirlinglem8  43629  fourierdlem50  43704  caragenval  44038  fargshiftfv  44902  lincvalsc0  45773  linc0scn0  45775  linc1  45777  lincscm  45782