Theorem fvmptg 5662

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373  ∃*wmo 2056   ∈ wcel 2177  {copab 4108   ↦ cmpt 4109  ‘cfv 5276

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3000  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-opab 4110  df-mpt 4111  df-id 4344  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-iota 5237  df-fun 5278  df-fv 5284

This theorem is referenced by:  fvmpt  5663  fvmpts  5664  fvmpt3  5665  fvmpt2  5670  f1mpt  5847  caofinvl  6191  1stvalg  6235  2ndvalg  6236  brtpos2  6344  rdgon  6479  frec0g  6490  freccllem  6495  frecfcllem  6497  frecsuclem  6499  sucinc  6538  sucinc2  6539  omcl  6554  oeicl  6555  oav2  6556  omv2  6558  fvdiagfn  6787  djulclr  7158  djurclr  7159  djulcl  7160  djurcl  7161  djulclb  7164  omp1eomlem  7203  ctmlemr  7217  nnnninf  7235  nnnninfeq  7237  cardval3ex  7299  ceilqval  10458  frec2uzzd  10552  frec2uzsucd  10553  monoord2  10638  iseqf1olemqval  10652  iseqf1olemqk  10659  seq3f1olemqsum  10665  seq3f1oleml  10668  seq3f1o  10669  seq3distr  10684  ser3le  10689  hashinfom  10930  hashennn  10932  cjval  11200  reval  11204  imval  11205  cvg1nlemcau  11339  cvg1nlemres  11340  absval  11356  resqrexlemglsq  11377  resqrexlemga  11378  climmpt  11655  climle  11689  climcvg1nlem  11704  summodclem3  11735  summodclem2a  11736  zsumdc  11739  fsum3  11742  fsumcl2lem  11753  sumsnf  11764  isumadd  11786  fsumrev  11798  fsumshft  11799  fsummulc2  11803  iserabs  11830  isumlessdc  11851  divcnv  11852  trireciplem  11855  trirecip  11856  expcnvap0  11857  expcnvre  11858  expcnv  11859  explecnv  11860  geolim  11866  geolim2  11867  geo2lim  11871  geoisum  11872  geoisumr  11873  geoisum1  11874  geoisum1c  11875  cvgratz  11887  mertenslem2  11891  mertensabs  11892  fprodmul  11946  eftvalcn  12012  efval  12016  efcvgfsum  12022  ege2le3  12026  efcj  12028  eftlub  12045  efgt1p2  12050  eflegeo  12056  sinval  12057  cosval  12058  tanvalap  12063  eirraplem  12132  phival  12579  crth  12590  phimullem  12591  ennnfonelemj0  12816  ennnfonelem0  12820  strnfvnd  12896  topnvalg  13127  tgval  13138  2idlval  14308  zrhval  14423  toponsspwpwg  14538  cldval  14615  ntrfval  14616  clsfval  14617  neifval  14656  neival  14659  ismet  14860  isxmet  14861  divcnap  15081  mulc1cncf  15105  djucllem  15810  nnsf  16016  peano3nninf  16018  nninfself  16024  nninfsellemeqinf  16027  dceqnconst  16073  dcapnconst  16074