Theorem fvmptg 5784

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 4195	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
9	7, 8	eqtri 2259	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)}
10	3, 4, 6, 9	fvopab3ig 5782	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶))
11	1, 10	mpi 15	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402  ∃*wmo 2087   ∈ wcel 2209  {copab 4192   ↦ cmpt 4193  ‘cfv 5380

This proof depends on 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 4251  ax-pow 4313  ax-pr 4348

This proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388

This theorem is used by:  fvmpt  5785  fvmpts  5786  fvmpt3  5787  fvmpt2  5792  f1mpt  5980  caofinvl  6332  1stvalg  6380  2ndvalg  6381  brtpos2  6526  rdgon  6661  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  sucinc  6722  sucinc2  6723  omcl  6738  oeicl  6739  oav2  6740  omv2  6742  fvdiagfn  6980  djulclr  7396  djurclr  7397  djulcl  7398  djurcl  7399  djulclb  7402  omp1eomlem  7441  ctmlemr  7455  nnnninf  7473  nnnninfeq  7475  cardval3ex  7537  ceilqval  10765  frec2uzzd  10859  frec2uzsucd  10860  monoord2  10945  iseqf1olemqval  10959  iseqf1olemqk  10966  seq3f1olemqsum  10972  seq3f1oleml  10975  seq3f1o  10976  seq3distr  10991  ser3le  10996  hashinfom  11240  hashennn  11242  cjval  11633  reval  11637  imval  11638  cvg1nlemcau  11773  cvg1nlemres  11774  absval  11790  resqrexlemglsq  11811  resqrexlemga  11812  climmpt  12092  climle  12126  climcvg1nlem  12141  summodclem3  12173  summodclem2a  12174  zsumdc  12177  fsum3  12180  fsumcl2lem  12191  sumsnf  12202  isumadd  12224  fsumrev  12236  fsumshft  12237  fsummulc2  12241  iserabs  12268  isumlessdc  12289  divcnv  12290  trireciplem  12293  trirecip  12294  expcnvap0  12295  expcnvre  12296  expcnv  12297  explecnv  12298  geolim  12304  geolim2  12305  geo2lim  12309  geoisum  12310  geoisumr  12311  geoisum1  12312  geoisum1c  12313  cvgratz  12325  mertenslem2  12329  mertensabs  12330  fprodmul  12384  eftvalcn  12450  efval  12454  efcvgfsum  12460  ege2le3  12464  efcj  12466  eftlub  12483  efgt1p2  12488  eflegeo  12494  sinval  12495  cosval  12496  tanvalap  12501  eirraplem  12570  phival  13021  crth  13032  phimullem  13033  ennnfonelemj0  13351  ennnfonelem0  13355  strnfvnd  13431  topnvalg  13665  tgval  13676  2idlval  14949  zrhval  15062  toponsspwpwg  15260  cldval  15337  ntrfval  15338  clsfval  15339  neifval  15378  neival  15381  ismet  15582  isxmet  15583  divcnap  15803  mulc1cncf  15827  depindlem1  16964  djucllem  17045  nnsf  17266  peano3nninf  17268  nninfself  17274  nninfsellemeqinf  17277  dceqnconst  17329  dcapnconst  17330