Theorem fvmptg 6977

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 2765	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2776	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2769	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 3673	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 5187	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2788	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 6975	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 21	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∃*wmo 2567  {copab 5167   ↦ cmpt 5186  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  fvmpti  6978  fvmpt  6979  fvmpt2f  6980  fvtresfn  6982  fvmpts  6983  fvmpt3  6984  fvmptd3  7003  fvmptss2  7006  f1mpt  7249  bropfvvvv  8075  tz7.44-3  8383  pw2f1olem  9057  wdom2d  9530  tz9.12lem3  9749  djurcl  9885  djur  9893  djuun  9900  cardval3  9926  cfval  10218  coftr  10245  fin1a2lem1  10372  fin1a2lem12  10383  axdc2lem  10420  pwcfsdom  10556  tskmval  10812  lsw  14591  swrdswrd  14732  trclfv  15027  relexpsucnnr  15052  dfrtrclrec2  15085  rtrclreclem2  15086  summolem2a  15756  prodmolem2a  15978  divsfval  17591  joinfval  18417  meetfval  18431  symgextfv  19479  symgextfve  19480  pmtrdifwrdel2lem1  19545  efgtf  19783  rrgsupp  20777  uvcvval  21896  ply1sclid  22409  submaval0  22698  m2detleiblem3  22747  m2detleiblem4  22748  maduval  22756  minmar1val0  22765  toponsspwpw  23040  cldval  23141  ntrfval  23142  clsfval  23143  opncldf3  23204  neifval  23217  lpfval  23256  islocfin  23635  kqfval  23841  stdbdxmet  24633  cmetcaulem  25408  bcth3  25451  itg2gt0  25880  ellimc2  25997  coe1termlem  26376  bdayval  27770  oldval  27985  clwlkclwwlkfo  30269  grpoinvfval  30783  grpodivfval  30795  nlfnval  32142  sigaval  34418  measval  34505  measdivcst  34531  measdivcstALTV  34532  probfinmeasbALTV  34736  ptpconn  35596  cvmsval  35629  ex-sategoelel12  35790  imageval  36291  fvimage  36292  tailfval  36745  tailval  36746  curfv  38111  heiborlem4  38325  lkrval  39724  cdleme31fv  41026  docavalN  41759  dochval  41987  mapdval  42264  hvmapval  42396  hvmapvalvalN  42397  hdmap1vallem  42433  hdmapval  42464  hgmapval  42523  mzpval  43325  mzpsubst  43341  pw2f1o2val  43628  refsum2cnlem1  45615  stoweidlem26  46598  stirlinglem8  46653  fourierdlem50  46728  caragenval  47065  nthrucw  47460  fargshiftfv  48043  lincvalsc0  49052  linc0scn0  49054  linc1  49056  lincscm  49061