Theorem fvmptg 5589

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353  ∃*wmo 2027   ∈ wcel 2148  {copab 4061   ↦ cmpt 4062  ‘cfv 5213

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-opab 4063  df-mpt 4064  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-iota 5175  df-fun 5215  df-fv 5221

This theorem is referenced by:  fvmpt  5590  fvmpts  5591  fvmpt3  5592  fvmpt2  5596  f1mpt  5767  caofinvl  6100  1stvalg  6138  2ndvalg  6139  brtpos2  6247  rdgon  6382  frec0g  6393  freccllem  6398  frecfcllem  6400  frecsuclem  6402  sucinc  6441  sucinc2  6442  omcl  6457  oeicl  6458  oav2  6459  omv2  6461  fvdiagfn  6688  djulclr  7043  djurclr  7044  djulcl  7045  djurcl  7046  djulclb  7049  omp1eomlem  7088  ctmlemr  7102  nnnninf  7119  nnnninfeq  7121  cardval3ex  7179  ceilqval  10299  frec2uzzd  10393  frec2uzsucd  10394  monoord2  10470  iseqf1olemqval  10480  iseqf1olemqk  10487  seq3f1olemqsum  10493  seq3f1oleml  10496  seq3f1o  10497  seq3distr  10506  ser3le  10511  hashinfom  10749  hashennn  10751  cjval  10845  reval  10849  imval  10850  cvg1nlemcau  10984  cvg1nlemres  10985  absval  11001  resqrexlemglsq  11022  resqrexlemga  11023  climmpt  11299  climle  11333  climcvg1nlem  11348  summodclem3  11379  summodclem2a  11380  zsumdc  11383  fsum3  11386  fsumcl2lem  11397  sumsnf  11408  isumadd  11430  fsumrev  11442  fsumshft  11443  fsummulc2  11447  iserabs  11474  isumlessdc  11495  divcnv  11496  trireciplem  11499  trirecip  11500  expcnvap0  11501  expcnvre  11502  expcnv  11503  explecnv  11504  geolim  11510  geolim2  11511  geo2lim  11515  geoisum  11516  geoisumr  11517  geoisum1  11518  geoisum1c  11519  cvgratz  11531  mertenslem2  11535  mertensabs  11536  fprodmul  11590  eftvalcn  11656  efval  11660  efcvgfsum  11666  ege2le3  11670  efcj  11672  eftlub  11689  efgt1p2  11694  eflegeo  11700  sinval  11701  cosval  11702  tanvalap  11707  eirraplem  11775  phival  12203  crth  12214  phimullem  12215  ennnfonelemj0  12392  ennnfonelem0  12396  strnfvnd  12472  topnvalg  12686  toponsspwpwg  13302  tgval  13331  cldval  13381  ntrfval  13382  clsfval  13383  neifval  13422  neival  13425  ismet  13626  isxmet  13627  divcnap  13837  mulc1cncf  13858  djucllem  14323  nnsf  14525  peano3nninf  14527  nninfself  14533  nninfsellemeqinf  14536  dceqnconst  14578  dcapnconst  14579