Theorem fvmptg 5613

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 2189	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2201	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2196	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2927	. . . 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 4081	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2210	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5611	. 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 1364   E*wmo 2039   e. wcel 2160   {copab 4078   |-> cmpt 4079   ` cfv 5235

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-iota 5196  df-fun 5237  df-fv 5243

This theorem is referenced by:  fvmpt  5614  fvmpts  5615  fvmpt3  5616  fvmpt2  5620  f1mpt  5793  caofinvl  6129  1stvalg  6167  2ndvalg  6168  brtpos2  6276  rdgon  6411  frec0g  6422  freccllem  6427  frecfcllem  6429  frecsuclem  6431  sucinc  6470  sucinc2  6471  omcl  6486  oeicl  6487  oav2  6488  omv2  6490  fvdiagfn  6719  djulclr  7078  djurclr  7079  djulcl  7080  djurcl  7081  djulclb  7084  omp1eomlem  7123  ctmlemr  7137  nnnninf  7154  nnnninfeq  7156  cardval3ex  7214  ceilqval  10337  frec2uzzd  10431  frec2uzsucd  10432  monoord2  10508  iseqf1olemqval  10518  iseqf1olemqk  10525  seq3f1olemqsum  10531  seq3f1oleml  10534  seq3f1o  10535  seq3distr  10544  ser3le  10549  hashinfom  10790  hashennn  10792  cjval  10886  reval  10890  imval  10891  cvg1nlemcau  11025  cvg1nlemres  11026  absval  11042  resqrexlemglsq  11063  resqrexlemga  11064  climmpt  11340  climle  11374  climcvg1nlem  11389  summodclem3  11420  summodclem2a  11421  zsumdc  11424  fsum3  11427  fsumcl2lem  11438  sumsnf  11449  isumadd  11471  fsumrev  11483  fsumshft  11484  fsummulc2  11488  iserabs  11515  isumlessdc  11536  divcnv  11537  trireciplem  11540  trirecip  11541  expcnvap0  11542  expcnvre  11543  expcnv  11544  explecnv  11545  geolim  11551  geolim2  11552  geo2lim  11556  geoisum  11557  geoisumr  11558  geoisum1  11559  geoisum1c  11560  cvgratz  11572  mertenslem2  11576  mertensabs  11577  fprodmul  11631  eftvalcn  11697  efval  11701  efcvgfsum  11707  ege2le3  11711  efcj  11713  eftlub  11730  efgt1p2  11735  eflegeo  11741  sinval  11742  cosval  11743  tanvalap  11748  eirraplem  11816  phival  12245  crth  12256  phimullem  12257  ennnfonelemj0  12452  ennnfonelem0  12456  strnfvnd  12532  topnvalg  12756  tgval  12767  toponsspwpwg  13979  cldval  14056  ntrfval  14057  clsfval  14058  neifval  14097  neival  14100  ismet  14301  isxmet  14302  divcnap  14512  mulc1cncf  14533  djucllem  15010  nnsf  15213  peano3nninf  15215  nninfself  15221  nninfsellemeqinf  15224  dceqnconst  15267  dcapnconst  15268