Theorem fvmptg 5755

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  ∃*wmo 2083   ∈ wcel 2205  {copab 4172   ↦ cmpt 4173  ‘cfv 5354

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 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-iota 5314  df-fun 5356  df-fv 5362

This theorem is referenced by:  fvmpt  5756  fvmpts  5757  fvmpt3  5758  fvmpt2  5763  f1mpt  5946  caofinvl  6294  1stvalg  6338  2ndvalg  6339  brtpos2  6484  rdgon  6619  frec0g  6630  freccllem  6635  frecfcllem  6637  frecsuclem  6639  sucinc  6680  sucinc2  6681  omcl  6696  oeicl  6697  oav2  6698  omv2  6700  fvdiagfn  6930  djulclr  7342  djurclr  7343  djulcl  7344  djurcl  7345  djulclb  7348  omp1eomlem  7387  ctmlemr  7401  nnnninf  7419  nnnninfeq  7421  cardval3ex  7483  ceilqval  10675  frec2uzzd  10769  frec2uzsucd  10770  monoord2  10855  iseqf1olemqval  10869  iseqf1olemqk  10876  seq3f1olemqsum  10882  seq3f1oleml  10885  seq3f1o  10886  seq3distr  10901  ser3le  10906  hashinfom  11149  hashennn  11151  cjval  11538  reval  11542  imval  11543  cvg1nlemcau  11677  cvg1nlemres  11678  absval  11694  resqrexlemglsq  11715  resqrexlemga  11716  climmpt  11993  climle  12027  climcvg1nlem  12042  summodclem3  12074  summodclem2a  12075  zsumdc  12078  fsum3  12081  fsumcl2lem  12092  sumsnf  12103  isumadd  12125  fsumrev  12137  fsumshft  12138  fsummulc2  12142  iserabs  12169  isumlessdc  12190  divcnv  12191  trireciplem  12194  trirecip  12195  expcnvap0  12196  expcnvre  12197  expcnv  12198  explecnv  12199  geolim  12205  geolim2  12206  geo2lim  12210  geoisum  12211  geoisumr  12212  geoisum1  12213  geoisum1c  12214  cvgratz  12226  mertenslem2  12230  mertensabs  12231  fprodmul  12285  eftvalcn  12351  efval  12355  efcvgfsum  12361  ege2le3  12365  efcj  12367  eftlub  12384  efgt1p2  12389  eflegeo  12395  sinval  12396  cosval  12397  tanvalap  12402  eirraplem  12471  phival  12918  crth  12929  phimullem  12930  ennnfonelemj0  13173  ennnfonelem0  13177  strnfvnd  13253  topnvalg  13485  tgval  13496  2idlval  14699  zrhval  14814  toponsspwpwg  14936  cldval  15013  ntrfval  15014  clsfval  15015  neifval  15054  neival  15057  ismet  15258  isxmet  15259  divcnap  15479  mulc1cncf  15503  depindlem1  16550  djucllem  16621  nnsf  16832  peano3nninf  16834  nninfself  16840  nninfsellemeqinf  16843  dceqnconst  16895  dcapnconst  16896