Theorem fvmptg 5449

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 2113	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2124	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2119	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2826	. . . 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 3949	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2133	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5447	. 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 1312   e. wcel 1461   E*wmo 1974   {copab 3946   |-> cmpt 3947   ` cfv 5079

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-sbc 2877  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-mpt 3949  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-iota 5044  df-fun 5081  df-fv 5087

This theorem is referenced by:  fvmpt  5450  fvmpts  5451  fvmpt3  5452  fvmpt2  5456  f1mpt  5624  caofinvl  5956  1stvalg  5992  2ndvalg  5993  brtpos2  6100  rdgon  6235  frec0g  6246  freccllem  6251  frecfcllem  6253  frecsuclem  6255  sucinc  6293  sucinc2  6294  omcl  6309  oeicl  6310  oav2  6311  omv2  6313  fvdiagfn  6539  djulclr  6884  djurclr  6885  djulcl  6886  djurcl  6887  djulclb  6890  omp1eomlem  6929  ctmlemr  6943  nnnninf  6971  cardval3ex  6988  ceilqval  9966  frec2uzzd  10060  frec2uzsucd  10061  monoord2  10137  iseqf1olemqval  10147  iseqf1olemqk  10154  seq3f1olemqsum  10160  seq3f1oleml  10163  seq3f1o  10164  seq3distr  10173  ser3le  10178  hashinfom  10411  hashennn  10413  cjval  10504  reval  10508  imval  10509  cvg1nlemcau  10642  cvg1nlemres  10643  absval  10659  resqrexlemglsq  10680  resqrexlemga  10681  climmpt  10955  climle  10989  climcvg1nlem  11004  summodclem3  11035  summodclem2a  11036  zsumdc  11039  fsum3  11042  fsumcl2lem  11053  sumsnf  11064  isumadd  11086  fsumrev  11098  fsumshft  11099  fsummulc2  11103  iserabs  11130  isumlessdc  11151  divcnv  11152  trireciplem  11155  trirecip  11156  expcnvap0  11157  expcnvre  11158  expcnv  11159  explecnv  11160  geolim  11166  geolim2  11167  geo2lim  11171  geoisum  11172  geoisumr  11173  geoisum1  11174  geoisum1c  11175  cvgratz  11187  mertenslem2  11191  mertensabs  11192  eftvalcn  11208  efval  11212  efcvgfsum  11218  ege2le3  11222  efcj  11224  eftlub  11241  efgt1p2  11246  eflegeo  11253  sinval  11254  cosval  11255  tanvalap  11260  eirraplem  11325  phival  11728  crth  11739  phimullem  11740  ennnfonelemj0  11753  ennnfonelem0  11757  strnfvnd  11816  topnvalg  11969  toponsspwpwg  12026  tgval  12055  cldval  12105  ntrfval  12106  clsfval  12107  neifval  12146  neival  12149  ismet  12327  isxmet  12328  divcnap  12535  mulc1cncf  12556  djucllem  12690  nnsf  12880  peano3nninf  12882  nninfalllemn  12883  nninfself  12890  nninfsellemeqinf  12893