Theorem fvmptg 6933

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 3662	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5175	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2756	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6931	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 20	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃*wmo 2535  {copab 5155   ↦ cmpt 5174  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmpti  6934  fvmpt  6935  fvmpt2f  6936  fvtresfn  6937  fvmpts  6938  fvmpt3  6939  fvmptd3  6958  fvmptss2  6961  f1mpt  7201  bropfvvvv  8028  tz7.44-3  8333  pw2f1olem  9001  wdom2d  9473  tz9.12lem3  9689  djurcl  9811  djur  9819  djuun  9826  cardval3  9852  cfval  10145  coftr  10171  fin1a2lem1  10298  fin1a2lem12  10309  axdc2lem  10346  pwcfsdom  10481  tskmval  10737  lsw  14473  swrdswrd  14614  trclfv  14909  relexpsucnnr  14934  dfrtrclrec2  14967  rtrclreclem2  14968  summolem2a  15624  prodmolem2a  15843  divsfval  17453  joinfval  18279  meetfval  18293  symgextfv  19332  symgextfve  19333  pmtrdifwrdel2lem1  19398  efgtf  19636  rrgsupp  20618  uvcvval  21725  ply1sclid  22203  submaval0  22496  m2detleiblem3  22545  m2detleiblem4  22546  maduval  22554  minmar1val0  22563  toponsspwpw  22838  cldval  22939  ntrfval  22940  clsfval  22941  opncldf3  23002  neifval  23015  lpfval  23054  islocfin  23433  kqfval  23639  stdbdxmet  24431  cmetcaulem  25216  bcth3  25259  itg2gt0  25689  ellimc2  25806  coe1termlem  26191  bdayval  27588  oldval  27796  clwlkclwwlkfo  29991  grpoinvfval  30504  grpodivfval  30516  nlfnval  31863  sigaval  34145  measval  34232  measdivcst  34258  measdivcstALTV  34259  probfinmeasbALTV  34463  ptpconn  35298  cvmsval  35331  ex-sategoelel12  35492  imageval  35993  fvimage  35994  tailfval  36437  tailval  36438  curfv  37660  heiborlem4  37874  lkrval  39207  cdleme31fv  40509  docavalN  41242  dochval  41470  mapdval  41747  hvmapval  41879  hvmapvalvalN  41880  hdmap1vallem  41916  hdmapval  41947  hgmapval  42006  mzpval  42849  mzpsubst  42865  pw2f1o2val  43156  refsum2cnlem1  45158  stoweidlem26  46148  stirlinglem8  46203  fourierdlem50  46278  caragenval  46615  nthrucw  47008  fargshiftfv  47563  lincvalsc0  48546  linc0scn0  48548  linc1  48550  lincscm  48555