Theorem fvmptg 5572

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 2170	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2182	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2177	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2905	. . . 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 4052	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2191	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5570	. 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 )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   E*wmo 2020   e. wcel 2141   {copab 4049   |-> cmpt 4050   ` cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-sbc 2956  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-iota 5160  df-fun 5200  df-fv 5206

This theorem is referenced by:  fvmpt  5573  fvmpts  5574  fvmpt3  5575  fvmpt2  5579  f1mpt  5750  caofinvl  6083  1stvalg  6121  2ndvalg  6122  brtpos2  6230  rdgon  6365  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  sucinc  6424  sucinc2  6425  omcl  6440  oeicl  6441  oav2  6442  omv2  6444  fvdiagfn  6671  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  djulclb  7032  omp1eomlem  7071  ctmlemr  7085  nnnninf  7102  nnnninfeq  7104  cardval3ex  7162  ceilqval  10262  frec2uzzd  10356  frec2uzsucd  10357  monoord2  10433  iseqf1olemqval  10443  iseqf1olemqk  10450  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  seq3distr  10469  ser3le  10474  hashinfom  10712  hashennn  10714  cjval  10809  reval  10813  imval  10814  cvg1nlemcau  10948  cvg1nlemres  10949  absval  10965  resqrexlemglsq  10986  resqrexlemga  10987  climmpt  11263  climle  11297  climcvg1nlem  11312  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsum3  11350  fsumcl2lem  11361  sumsnf  11372  isumadd  11394  fsumrev  11406  fsumshft  11407  fsummulc2  11411  iserabs  11438  isumlessdc  11459  divcnv  11460  trireciplem  11463  trirecip  11464  expcnvap0  11465  expcnvre  11466  expcnv  11467  explecnv  11468  geolim  11474  geolim2  11475  geo2lim  11479  geoisum  11480  geoisumr  11481  geoisum1  11482  geoisum1c  11483  cvgratz  11495  mertenslem2  11499  mertensabs  11500  fprodmul  11554  eftvalcn  11620  efval  11624  efcvgfsum  11630  ege2le3  11634  efcj  11636  eftlub  11653  efgt1p2  11658  eflegeo  11664  sinval  11665  cosval  11666  tanvalap  11671  eirraplem  11739  phival  12167  crth  12178  phimullem  12179  ennnfonelemj0  12356  ennnfonelem0  12360  strnfvnd  12436  topnvalg  12591  toponsspwpwg  12814  tgval  12843  cldval  12893  ntrfval  12894  clsfval  12895  neifval  12934  neival  12937  ismet  13138  isxmet  13139  divcnap  13349  mulc1cncf  13370  djucllem  13835  nnsf  14038  peano3nninf  14040  nninfself  14046  nninfsellemeqinf  14049  dceqnconst  14091  dcapnconst  14092