Theorem fvmptg 5752

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃*wmo 2081   ∈ wcel 2203  {copab 4169   ↦ cmpt 4170  ‘cfv 5351

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-mpt 4172  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359

This theorem is referenced by:  fvmpt  5753  fvmpts  5754  fvmpt3  5755  fvmpt2  5760  f1mpt  5943  caofinvl  6291  1stvalg  6335  2ndvalg  6336  brtpos2  6481  rdgon  6616  frec0g  6627  freccllem  6632  frecfcllem  6634  frecsuclem  6636  sucinc  6677  sucinc2  6678  omcl  6693  oeicl  6694  oav2  6695  omv2  6697  fvdiagfn  6927  djulclr  7339  djurclr  7340  djulcl  7341  djurcl  7342  djulclb  7345  omp1eomlem  7384  ctmlemr  7398  nnnninf  7416  nnnninfeq  7418  cardval3ex  7480  ceilqval  10664  frec2uzzd  10758  frec2uzsucd  10759  monoord2  10844  iseqf1olemqval  10858  iseqf1olemqk  10865  seq3f1olemqsum  10871  seq3f1oleml  10874  seq3f1o  10875  seq3distr  10890  ser3le  10895  hashinfom  11136  hashennn  11138  cjval  11523  reval  11527  imval  11528  cvg1nlemcau  11662  cvg1nlemres  11663  absval  11679  resqrexlemglsq  11700  resqrexlemga  11701  climmpt  11978  climle  12012  climcvg1nlem  12027  summodclem3  12059  summodclem2a  12060  zsumdc  12063  fsum3  12066  fsumcl2lem  12077  sumsnf  12088  isumadd  12110  fsumrev  12122  fsumshft  12123  fsummulc2  12127  iserabs  12154  isumlessdc  12175  divcnv  12176  trireciplem  12179  trirecip  12180  expcnvap0  12181  expcnvre  12182  expcnv  12183  explecnv  12184  geolim  12190  geolim2  12191  geo2lim  12195  geoisum  12196  geoisumr  12197  geoisum1  12198  geoisum1c  12199  cvgratz  12211  mertenslem2  12215  mertensabs  12216  fprodmul  12270  eftvalcn  12336  efval  12340  efcvgfsum  12346  ege2le3  12350  efcj  12352  eftlub  12369  efgt1p2  12374  eflegeo  12380  sinval  12381  cosval  12382  tanvalap  12387  eirraplem  12456  phival  12903  crth  12914  phimullem  12915  ennnfonelemj0  13141  ennnfonelem0  13145  strnfvnd  13221  topnvalg  13453  tgval  13464  2idlval  14637  zrhval  14752  toponsspwpwg  14874  cldval  14951  ntrfval  14952  clsfval  14953  neifval  14992  neival  14995  ismet  15196  isxmet  15197  divcnap  15417  mulc1cncf  15441  depindlem1  16488  djucllem  16559  nnsf  16770  peano3nninf  16772  nninfself  16778  nninfsellemeqinf  16781  dceqnconst  16832  dcapnconst  16833