Theorem fvmptg 5593

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 2177	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2189	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2184	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2913	. . . 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 4067	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2198	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5591	. 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 104   = wceq 1353   E*wmo 2027   e. wcel 2148   {copab 4064   |-> cmpt 4065   ` cfv 5217

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-sbc 2964  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-iota 5179  df-fun 5219  df-fv 5225

This theorem is referenced by:  fvmpt  5594  fvmpts  5595  fvmpt3  5596  fvmpt2  5600  f1mpt  5772  caofinvl  6105  1stvalg  6143  2ndvalg  6144  brtpos2  6252  rdgon  6387  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  sucinc  6446  sucinc2  6447  omcl  6462  oeicl  6463  oav2  6464  omv2  6466  fvdiagfn  6693  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djulclb  7054  omp1eomlem  7093  ctmlemr  7107  nnnninf  7124  nnnninfeq  7126  cardval3ex  7184  ceilqval  10306  frec2uzzd  10400  frec2uzsucd  10401  monoord2  10477  iseqf1olemqval  10487  iseqf1olemqk  10494  seq3f1olemqsum  10500  seq3f1oleml  10503  seq3f1o  10504  seq3distr  10513  ser3le  10518  hashinfom  10758  hashennn  10760  cjval  10854  reval  10858  imval  10859  cvg1nlemcau  10993  cvg1nlemres  10994  absval  11010  resqrexlemglsq  11031  resqrexlemga  11032  climmpt  11308  climle  11342  climcvg1nlem  11357  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsum3  11395  fsumcl2lem  11406  sumsnf  11417  isumadd  11439  fsumrev  11451  fsumshft  11452  fsummulc2  11456  iserabs  11483  isumlessdc  11504  divcnv  11505  trireciplem  11508  trirecip  11509  expcnvap0  11510  expcnvre  11511  expcnv  11512  explecnv  11513  geolim  11519  geolim2  11520  geo2lim  11524  geoisum  11525  geoisumr  11526  geoisum1  11527  geoisum1c  11528  cvgratz  11540  mertenslem2  11544  mertensabs  11545  fprodmul  11599  eftvalcn  11665  efval  11669  efcvgfsum  11675  ege2le3  11679  efcj  11681  eftlub  11698  efgt1p2  11703  eflegeo  11709  sinval  11710  cosval  11711  tanvalap  11716  eirraplem  11784  phival  12213  crth  12224  phimullem  12225  ennnfonelemj0  12402  ennnfonelem0  12406  strnfvnd  12482  topnvalg  12700  tgval  12711  toponsspwpwg  13525  cldval  13602  ntrfval  13603  clsfval  13604  neifval  13643  neival  13646  ismet  13847  isxmet  13848  divcnap  14058  mulc1cncf  14079  djucllem  14555  nnsf  14757  peano3nninf  14759  nninfself  14765  nninfsellemeqinf  14768  dceqnconst  14810  dcapnconst  14811