Theorem fvmptg 6966

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃*wmo 2531  {copab 5169   ↦ cmpt 5188  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fvmpti  6967  fvmpt  6968  fvmpt2f  6969  fvtresfn  6970  fvmpts  6971  fvmpt3  6972  fvmptd3  6991  fvmptss2  6994  f1mpt  7236  bropfvvvv  8071  tz7.44-3  8376  pw2f1olem  9045  wdom2d  9533  tz9.12lem3  9742  djurcl  9864  djur  9872  djuun  9879  cardval3  9905  cfval  10200  coftr  10226  fin1a2lem1  10353  fin1a2lem12  10364  axdc2lem  10401  pwcfsdom  10536  tskmval  10792  lsw  14529  swrdswrd  14670  trclfv  14966  relexpsucnnr  14991  dfrtrclrec2  15024  rtrclreclem2  15025  summolem2a  15681  prodmolem2a  15900  divsfval  17510  joinfval  18332  meetfval  18346  symgextfv  19348  symgextfve  19349  pmtrdifwrdel2lem1  19414  efgtf  19652  rrgsupp  20610  uvcvval  21695  ply1sclid  22174  submaval0  22467  m2detleiblem3  22516  m2detleiblem4  22517  maduval  22525  minmar1val0  22534  toponsspwpw  22809  cldval  22910  ntrfval  22911  clsfval  22912  opncldf3  22973  neifval  22986  lpfval  23025  islocfin  23404  kqfval  23610  stdbdxmet  24403  cmetcaulem  25188  bcth3  25231  itg2gt0  25661  ellimc2  25778  coe1termlem  26163  bdayval  27560  oldval  27762  clwlkclwwlkfo  29938  grpoinvfval  30451  grpodivfval  30463  nlfnval  31810  sigaval  34101  measval  34188  measdivcst  34214  measdivcstALTV  34215  probfinmeasbALTV  34420  ptpconn  35220  cvmsval  35253  ex-sategoelel12  35414  imageval  35918  fvimage  35919  tailfval  36360  tailval  36361  curfv  37594  heiborlem4  37808  lkrval  39081  cdleme31fv  40384  docavalN  41117  dochval  41345  mapdval  41622  hvmapval  41754  hvmapvalvalN  41755  hdmap1vallem  41791  hdmapval  41822  hgmapval  41881  mzpval  42720  mzpsubst  42736  pw2f1o2val  43028  refsum2cnlem1  45031  stoweidlem26  46024  stirlinglem8  46079  fourierdlem50  46154  caragenval  46491  fargshiftfv  47440  lincvalsc0  48410  linc0scn0  48412  linc1  48414  lincscm  48419