Theorem fvmptg 5634

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 2193	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2205	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2200	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2936	. . . 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 4093	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2214	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5632	. 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 2043   e. wcel 2164   {copab 4090   |-> cmpt 4091   ` cfv 5255

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 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2987  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-mpt 4093  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263

This theorem is referenced by:  fvmpt  5635  fvmpts  5636  fvmpt3  5637  fvmpt2  5642  f1mpt  5815  caofinvl  6157  1stvalg  6197  2ndvalg  6198  brtpos2  6306  rdgon  6441  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  sucinc  6500  sucinc2  6501  omcl  6516  oeicl  6517  oav2  6518  omv2  6520  fvdiagfn  6749  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  djulclb  7116  omp1eomlem  7155  ctmlemr  7169  nnnninf  7187  nnnninfeq  7189  cardval3ex  7247  ceilqval  10380  frec2uzzd  10474  frec2uzsucd  10475  monoord2  10560  iseqf1olemqval  10574  iseqf1olemqk  10581  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  seq3distr  10606  ser3le  10611  hashinfom  10852  hashennn  10854  cjval  10992  reval  10996  imval  10997  cvg1nlemcau  11131  cvg1nlemres  11132  absval  11148  resqrexlemglsq  11169  resqrexlemga  11170  climmpt  11446  climle  11480  climcvg1nlem  11495  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsum3  11533  fsumcl2lem  11544  sumsnf  11555  isumadd  11577  fsumrev  11589  fsumshft  11590  fsummulc2  11594  iserabs  11621  isumlessdc  11642  divcnv  11643  trireciplem  11646  trirecip  11647  expcnvap0  11648  expcnvre  11649  expcnv  11650  explecnv  11651  geolim  11657  geolim2  11658  geo2lim  11662  geoisum  11663  geoisumr  11664  geoisum1  11665  geoisum1c  11666  cvgratz  11678  mertenslem2  11682  mertensabs  11683  fprodmul  11737  eftvalcn  11803  efval  11807  efcvgfsum  11813  ege2le3  11817  efcj  11819  eftlub  11836  efgt1p2  11841  eflegeo  11847  sinval  11848  cosval  11849  tanvalap  11854  eirraplem  11923  phival  12354  crth  12365  phimullem  12366  ennnfonelemj0  12561  ennnfonelem0  12565  strnfvnd  12641  topnvalg  12865  tgval  12876  2idlval  14001  zrhval  14116  toponsspwpwg  14201  cldval  14278  ntrfval  14279  clsfval  14280  neifval  14319  neival  14322  ismet  14523  isxmet  14524  divcnap  14744  mulc1cncf  14768  djucllem  15362  nnsf  15565  peano3nninf  15567  nninfself  15573  nninfsellemeqinf  15576  dceqnconst  15620  dcapnconst  15621