Theorem fvmptg 5605

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 2187	. 2 ⊢ 𝐶 = 𝐶
2		fvmptg.1	. . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	eqeq2d 2199	. . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶))
4		eqeq1 2194	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶))
5		moeq 2924	. . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵
6	5	a1i 9	. . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵)
7		fvmptg.2	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
8		df-mpt 4078	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2208	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 5603	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 15	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1363  ∃*wmo 2037   ∈ wcel 2158  {copab 4075   ↦ cmpt 4076  ‘cfv 5228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-sbc 2975  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-iota 5190  df-fun 5230  df-fv 5236

This theorem is referenced by:  fvmpt  5606  fvmpts  5607  fvmpt3  5608  fvmpt2  5612  f1mpt  5785  caofinvl  6119  1stvalg  6157  2ndvalg  6158  brtpos2  6266  rdgon  6401  frec0g  6412  freccllem  6417  frecfcllem  6419  frecsuclem  6421  sucinc  6460  sucinc2  6461  omcl  6476  oeicl  6477  oav2  6478  omv2  6480  fvdiagfn  6707  djulclr  7062  djurclr  7063  djulcl  7064  djurcl  7065  djulclb  7068  omp1eomlem  7107  ctmlemr  7121  nnnninf  7138  nnnninfeq  7140  cardval3ex  7198  ceilqval  10320  frec2uzzd  10414  frec2uzsucd  10415  monoord2  10491  iseqf1olemqval  10501  iseqf1olemqk  10508  seq3f1olemqsum  10514  seq3f1oleml  10517  seq3f1o  10518  seq3distr  10527  ser3le  10532  hashinfom  10772  hashennn  10774  cjval  10868  reval  10872  imval  10873  cvg1nlemcau  11007  cvg1nlemres  11008  absval  11024  resqrexlemglsq  11045  resqrexlemga  11046  climmpt  11322  climle  11356  climcvg1nlem  11371  summodclem3  11402  summodclem2a  11403  zsumdc  11406  fsum3  11409  fsumcl2lem  11420  sumsnf  11431  isumadd  11453  fsumrev  11465  fsumshft  11466  fsummulc2  11470  iserabs  11497  isumlessdc  11518  divcnv  11519  trireciplem  11522  trirecip  11523  expcnvap0  11524  expcnvre  11525  expcnv  11526  explecnv  11527  geolim  11533  geolim2  11534  geo2lim  11538  geoisum  11539  geoisumr  11540  geoisum1  11541  geoisum1c  11542  cvgratz  11554  mertenslem2  11558  mertensabs  11559  fprodmul  11613  eftvalcn  11679  efval  11683  efcvgfsum  11689  ege2le3  11693  efcj  11695  eftlub  11712  efgt1p2  11717  eflegeo  11723  sinval  11724  cosval  11725  tanvalap  11730  eirraplem  11798  phival  12227  crth  12238  phimullem  12239  ennnfonelemj0  12416  ennnfonelem0  12420  strnfvnd  12496  topnvalg  12718  tgval  12729  toponsspwpwg  13875  cldval  13952  ntrfval  13953  clsfval  13954  neifval  13993  neival  13996  ismet  14197  isxmet  14198  divcnap  14408  mulc1cncf  14429  djucllem  14905  nnsf  15108  peano3nninf  15110  nninfself  15116  nninfsellemeqinf  15119  dceqnconst  15162  dcapnconst  15163