Theorem fvmptg 6994

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃*wmo 2533  {copab 5210   ↦ cmpt 5231  ‘cfv 6541

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 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6493  df-fun 6543  df-fv 6549

This theorem is referenced by:  fvmpti  6995  fvmpt  6996  fvmpt2f  6997  fvtresfn  6998  fvmpts  6999  fvmpt3  7000  fvmptd3  7019  fvmptss2  7021  f1mpt  7257  bropfvvvv  8075  tz7.44-3  8405  pw2f1olem  9073  wdom2d  9572  tz9.12lem3  9781  djurcl  9903  djur  9911  djuun  9918  cardval3  9944  cfval  10239  coftr  10265  fin1a2lem1  10392  fin1a2lem12  10403  axdc2lem  10440  pwcfsdom  10575  tskmval  10831  lsw  14511  swrdswrd  14652  trclfv  14944  relexpsucnnr  14969  dfrtrclrec2  15002  rtrclreclem2  15003  summolem2a  15658  prodmolem2a  15875  divsfval  17490  joinfval  18323  meetfval  18337  symgextfv  19281  symgextfve  19282  pmtrdifwrdel2lem1  19347  efgtf  19585  rrgsupp  20900  uvcvval  21333  ply1sclid  21802  submaval0  22074  m2detleiblem3  22123  m2detleiblem4  22124  maduval  22132  minmar1val0  22141  toponsspwpw  22416  cldval  22519  ntrfval  22520  clsfval  22521  opncldf3  22582  neifval  22595  lpfval  22634  islocfin  23013  kqfval  23219  stdbdxmet  24016  cmetcaulem  24797  bcth3  24840  itg2gt0  25270  ellimc2  25386  coe1termlem  25764  bdayval  27141  oldval  27339  clwlkclwwlkfo  29252  grpoinvfval  29763  grpodivfval  29775  nlfnval  31122  sigaval  33098  measval  33185  measdivcst  33211  measdivcstALTV  33212  probfinmeasbALTV  33417  ptpconn  34213  cvmsval  34246  ex-sategoelel12  34407  imageval  34891  fvimage  34892  tailfval  35246  tailval  35247  curfv  36457  heiborlem4  36671  lkrval  37947  cdleme31fv  39250  docavalN  39983  dochval  40211  mapdval  40488  hvmapval  40620  hvmapvalvalN  40621  hdmap1vallem  40657  hdmapval  40688  hgmapval  40747  mzpval  41456  mzpsubst  41472  pw2f1o2val  41764  refsum2cnlem1  43707  stoweidlem26  44729  stirlinglem8  44784  fourierdlem50  44859  caragenval  45196  fargshiftfv  46094  lincvalsc0  47056  linc0scn0  47058  linc1  47060  lincscm  47065