Theorem fvmptg 5683

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1375  ∃*wmo 2058   ∈ wcel 2180  {copab 4123   ↦ cmpt 4124  ‘cfv 5294

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-sbc 3009  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-iota 5254  df-fun 5296  df-fv 5302

This theorem is referenced by:  fvmpt  5684  fvmpts  5685  fvmpt3  5686  fvmpt2  5691  f1mpt  5868  caofinvl  6214  1stvalg  6258  2ndvalg  6259  brtpos2  6367  rdgon  6502  frec0g  6513  freccllem  6518  frecfcllem  6520  frecsuclem  6522  sucinc  6561  sucinc2  6562  omcl  6577  oeicl  6578  oav2  6579  omv2  6581  fvdiagfn  6810  djulclr  7184  djurclr  7185  djulcl  7186  djurcl  7187  djulclb  7190  omp1eomlem  7229  ctmlemr  7243  nnnninf  7261  nnnninfeq  7263  cardval3ex  7325  ceilqval  10495  frec2uzzd  10589  frec2uzsucd  10590  monoord2  10675  iseqf1olemqval  10689  iseqf1olemqk  10696  seq3f1olemqsum  10702  seq3f1oleml  10705  seq3f1o  10706  seq3distr  10721  ser3le  10726  hashinfom  10967  hashennn  10969  cjval  11322  reval  11326  imval  11327  cvg1nlemcau  11461  cvg1nlemres  11462  absval  11478  resqrexlemglsq  11499  resqrexlemga  11500  climmpt  11777  climle  11811  climcvg1nlem  11826  summodclem3  11857  summodclem2a  11858  zsumdc  11861  fsum3  11864  fsumcl2lem  11875  sumsnf  11886  isumadd  11908  fsumrev  11920  fsumshft  11921  fsummulc2  11925  iserabs  11952  isumlessdc  11973  divcnv  11974  trireciplem  11977  trirecip  11978  expcnvap0  11979  expcnvre  11980  expcnv  11981  explecnv  11982  geolim  11988  geolim2  11989  geo2lim  11993  geoisum  11994  geoisumr  11995  geoisum1  11996  geoisum1c  11997  cvgratz  12009  mertenslem2  12013  mertensabs  12014  fprodmul  12068  eftvalcn  12134  efval  12138  efcvgfsum  12144  ege2le3  12148  efcj  12150  eftlub  12167  efgt1p2  12172  eflegeo  12178  sinval  12179  cosval  12180  tanvalap  12185  eirraplem  12254  phival  12701  crth  12712  phimullem  12713  ennnfonelemj0  12938  ennnfonelem0  12942  strnfvnd  13018  topnvalg  13250  tgval  13261  2idlval  14431  zrhval  14546  toponsspwpwg  14661  cldval  14738  ntrfval  14739  clsfval  14740  neifval  14779  neival  14782  ismet  14983  isxmet  14984  divcnap  15204  mulc1cncf  15228  djucllem  16074  nnsf  16282  peano3nninf  16284  nninfself  16290  nninfsellemeqinf  16293  dceqnconst  16339  dcapnconst  16340