Theorem fvmptg 6991

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∃*wmo 2562  {copab 5166   ↦ cmpt 5185  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is used by:  fvmpti  6992  fvmpt  6993  fvmpt2f  6994  fvtresfn  6996  fvmpts  6997  fvmpt3  6998  fvmptd3  7017  fvmptss2  7020  f1mpt  7265  bropfvvvv  8103  tz7.44-3  8419  curfv  8895  pw2f1olem  9103  wdom2d  9577  tz9.12lem3  9799  djurcl  9995  djur  10003  djuun  10010  cardval3  10036  cfval  10327  coftr  10354  fin1a2lem1  10481  fin1a2lem12  10492  axdc2lem  10529  pwcfsdom  10671  tskmval  10927  lsw  14712  swrdswrd  14858  trclfv  15158  relexpsucnnr  15183  dfrtrclrec2  15216  rtrclreclem2  15217  summolem2a  15886  prodmolem2a  16106  divsfval  17724  joinfval  18550  meetfval  18564  symgextfv  19637  symgextfve  19638  pmtrdifwrdel2lem1  19703  efgtf  19941  rrgsupp  20958  uvcvval  22097  ply1sclid  22612  submaval0  22900  m2detleiblem3  22949  m2detleiblem4  22950  maduval  22958  minmar1val0  22967  toponsspwpw  23245  cldval  23346  ntrfval  23347  clsfval  23348  opncldf3  23409  neifval  23422  lpfval  23461  islocfin  23841  kqfval  24047  stdbdxmet  24839  cmetcaulem  25614  bcth3  25657  itg2gt0  26086  ellimc2  26202  coe1termlem  26582  bdayval  28010  oldval  28225  clwlkclwwlkfo  30605  grpoinvfval  31129  grpodivfval  31141  nlfnval  32488  sigaval  34789  measval  34877  measdivcst  34903  measdivcstALTV  34904  probfinmeasbALTV  35107  ptpconn  36084  cvmsval  36117  ex-sategoelel12  36278  mirimanoffr  36546  imageval  36784  fvimage  36785  tailfval  37252  tailval  37253  heiborlem4  38841  lkrval  40238  cdleme31fv  41540  docavalN  42273  dochval  42501  mapdval  42778  hvmapval  42910  hvmapvalvalN  42911  hdmap1vallem  42947  hdmapval  42978  hgmapval  43037  mzpval  43836  mzpsubst  43852  pw2f1o2val  44139  refsum2cnlem1  46147  stoweidlem26  47129  stirlinglem8  47184  fourierdlem50  47259  caragenval  47596  fargshiftfv  48614  lincvalsc0  49626  linc0scn0  49628  linc1  49630  lincscm  49635