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	|- ( x = A -> B = C )
fvmptg.2	|- F = ( x e. D |-> B )

Assertion

Ref	Expression
fvmptg	|- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

Distinct variable groups:   x, A   x, C   x, D

Allowed substitution hints:   B( x)   R( x)   F( x)

Proof of Theorem fvmptg

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2238	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2250	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2245	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3001	. . . 4 |- E* y y = B
6	5	a1i 9	. . 3 |- ( x e. D -> E* y y = B )
7		fvmptg.2	. . . 4 |- F = ( x e. D |-> B )
8		df-mpt 4195	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2259	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5782	. 2 |- ( ( A e. D /\ C e. R ) -> ( C = C -> ( F ` A ) = C ) )
11	1, 10	mpi 15	1 |- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   E*wmo 2087   e. 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  6527  rdgon  6662  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  sucinc  6723  sucinc2  6724  omcl  6739  oeicl  6740  oav2  6741  omv2  6743  fvdiagfn  6981  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djulclb  7401  omp1eomlem  7440  ctmlemr  7454  nnnninf  7472  nnnninfeq  7474  cardval3ex  7536  ceilqval  10763  frec2uzzd  10857  frec2uzsucd  10858  monoord2  10943  iseqf1olemqval  10957  iseqf1olemqk  10964  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  seq3distr  10989  ser3le  10994  hashinfom  11238  hashennn  11240  cjval  11631  reval  11635  imval  11636  cvg1nlemcau  11771  cvg1nlemres  11772  absval  11788  resqrexlemglsq  11809  resqrexlemga  11810  climmpt  12090  climle  12124  climcvg1nlem  12139  summodclem3  12171  summodclem2a  12172  zsumdc  12175  fsum3  12178  fsumcl2lem  12189  sumsnf  12200  isumadd  12222  fsumrev  12234  fsumshft  12235  fsummulc2  12239  iserabs  12266  isumlessdc  12287  divcnv  12288  trireciplem  12291  trirecip  12292  expcnvap0  12293  expcnvre  12294  expcnv  12295  explecnv  12296  geolim  12302  geolim2  12303  geo2lim  12307  geoisum  12308  geoisumr  12309  geoisum1  12310  geoisum1c  12311  cvgratz  12323  mertenslem2  12327  mertensabs  12328  fprodmul  12382  eftvalcn  12448  efval  12452  efcvgfsum  12458  ege2le3  12462  efcj  12464  eftlub  12481  efgt1p2  12486  eflegeo  12492  sinval  12493  cosval  12494  tanvalap  12499  eirraplem  12568  phival  13019  crth  13030  phimullem  13031  ennnfonelemj0  13349  ennnfonelem0  13353  strnfvnd  13429  topnvalg  13663  tgval  13674  2idlval  14947  zrhval  15060  toponsspwpwg  15265  cldval  15342  ntrfval  15343  clsfval  15344  neifval  15383  neival  15386  ismet  15587  isxmet  15588  divcnap  15808  mulc1cncf  15832  depindlem1  16969  djucllem  17050  nnsf  17271  peano3nninf  17273  nninfself  17279  nninfsellemeqinf  17282  dceqnconst  17334  dcapnconst  17335