Theorem fvmptg 5393

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1290   ∈ wcel 1439  ∃*wmo 1950  {copab 3904   ↦ cmpt 3905  ‘cfv 5028

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2622  df-sbc 2842  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-opab 3906  df-mpt 3907  df-id 4129  df-xp 4457  df-rel 4458  df-cnv 4459  df-co 4460  df-dm 4461  df-iota 4993  df-fun 5030  df-fv 5036

This theorem is referenced by:  fvmpt  5394  fvmpts  5395  fvmpt3  5396  fvmpt2  5399  f1mpt  5564  fnofval  5879  caofinvl  5891  1stvalg  5927  2ndvalg  5928  brtpos2  6030  rdgon  6165  frec0g  6176  freccllem  6181  frecfcllem  6183  frecsuclem  6185  sucinc  6220  sucinc2  6221  omcl  6236  oeicl  6237  oav2  6238  omv2  6240  fvdiagfn  6464  djulclr  6795  djurclr  6796  djulcl  6797  djurcl  6798  djulclb  6801  djur  6811  fodjuomnilemm  6855  fodjuomnilem0  6856  nnnninf  6860  cardval3ex  6867  ceilqval  9767  frec2uzzd  9861  frec2uzsucd  9862  monoord2  9959  iseqf1olemqval  9970  iseqf1olemqk  9977  seq3f1olemqsum  9983  seq3f1oleml  9986  seq3f1o  9987  iseqdistr  9999  seq3distr  10000  ser3le  10007  hashinfom  10240  hashennn  10242  cjval  10333  reval  10337  imval  10338  cvg1nlemcau  10471  cvg1nlemres  10472  absval  10488  resqrexlemglsq  10509  resqrexlemga  10510  climmpt  10742  climle  10776  climcvg1nlem  10792  isummolem3  10824  isummolem2a  10825  zisum  10828  fisum  10832  fsum3  10833  fsumf1o  10836  fisumser  10844  fsumcl2lem  10846  fsumadd  10854  sumsnf  10857  isumadd  10879  fsumrev  10891  fsumshft  10892  fsummulc2  10896  iserabs  10923  isumlessdc  10944  divcnv  10945  trireciplem  10948  trirecip  10949  expcnvap0  10950  expcnvre  10951  expcnv  10952  explecnv  10953  geolim  10959  geolim2  10960  geo2lim  10964  geoisum  10965  geoisumr  10966  geoisum1  10967  geoisum1c  10968  cvgratz  10980  mertenslem2  10984  mertensabs  10985  eftvalcn  11001  efval  11005  efcvgfsum  11011  ege2le3  11015  efcj  11017  eftlub  11034  efgt1p2  11039  eflegeo  11046  sinval  11047  cosval  11048  tanvalap  11053  eirraplem  11118  phival  11521  crth  11532  phimullem  11533  strnfvnd  11568  topnvalg  11718  toponsspwpwg  11774  tgval  11803  cldval  11853  ntrfval  11854  clsfval  11855  mulc1cncf  11911  djucllem  11966  nnsf  12161  peano3nninf  12163  nninfalllemn  12164  nninfself  12171  nninfsellemeqinf  12174