Theorem fvmptg 5778

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402  ∃*wmo 2087   ∈ wcel 2209  {copab 4189   ↦ cmpt 4190  ‘cfv 5375

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-iota 5335  df-fun 5377  df-fv 5383

This theorem is referenced by:  fvmpt  5779  fvmpts  5780  fvmpt3  5781  fvmpt2  5786  f1mpt  5971  caofinvl  6322  1stvalg  6370  2ndvalg  6371  brtpos2  6516  rdgon  6651  frec0g  6662  freccllem  6667  frecfcllem  6669  frecsuclem  6671  sucinc  6712  sucinc2  6713  omcl  6728  oeicl  6729  oav2  6730  omv2  6732  fvdiagfn  6969  djulclr  7383  djurclr  7384  djulcl  7385  djurcl  7386  djulclb  7389  omp1eomlem  7428  ctmlemr  7442  nnnninf  7460  nnnninfeq  7462  cardval3ex  7524  ceilqval  10726  frec2uzzd  10820  frec2uzsucd  10821  monoord2  10906  iseqf1olemqval  10920  iseqf1olemqk  10927  seq3f1olemqsum  10933  seq3f1oleml  10936  seq3f1o  10937  seq3distr  10952  ser3le  10957  hashinfom  11200  hashennn  11202  cjval  11593  reval  11597  imval  11598  cvg1nlemcau  11733  cvg1nlemres  11734  absval  11750  resqrexlemglsq  11771  resqrexlemga  11772  climmpt  12049  climle  12083  climcvg1nlem  12098  summodclem3  12130  summodclem2a  12131  zsumdc  12134  fsum3  12137  fsumcl2lem  12148  sumsnf  12159  isumadd  12181  fsumrev  12193  fsumshft  12194  fsummulc2  12198  iserabs  12225  isumlessdc  12246  divcnv  12247  trireciplem  12250  trirecip  12251  expcnvap0  12252  expcnvre  12253  expcnv  12254  explecnv  12255  geolim  12261  geolim2  12262  geo2lim  12266  geoisum  12267  geoisumr  12268  geoisum1  12269  geoisum1c  12270  cvgratz  12282  mertenslem2  12286  mertensabs  12287  fprodmul  12341  eftvalcn  12407  efval  12411  efcvgfsum  12417  ege2le3  12421  efcj  12423  eftlub  12440  efgt1p2  12445  eflegeo  12451  sinval  12452  cosval  12453  tanvalap  12458  eirraplem  12527  phival  12974  crth  12985  phimullem  12986  ennnfonelemj0  13275  ennnfonelem0  13279  strnfvnd  13355  topnvalg  13588  tgval  13599  2idlval  14822  zrhval  14935  toponsspwpwg  15106  cldval  15183  ntrfval  15184  clsfval  15185  neifval  15224  neival  15227  ismet  15428  isxmet  15429  divcnap  15649  mulc1cncf  15673  depindlem1  16730  djucllem  16811  nnsf  17022  peano3nninf  17024  nninfself  17030  nninfsellemeqinf  17033  dceqnconst  17084  dcapnconst  17085