Theorem fvmptg 5570

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 4050	. . . 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 5568	. 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 4047   |-> cmpt 4048   ` cfv 5196

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 4105  ax-pow 4158  ax-pr 4192

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 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-opab 4049  df-mpt 4050  df-id 4276  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-iota 5158  df-fun 5198  df-fv 5204

This theorem is referenced by:  fvmpt  5571  fvmpts  5572  fvmpt3  5573  fvmpt2  5577  f1mpt  5747  caofinvl  6080  1stvalg  6118  2ndvalg  6119  brtpos2  6227  rdgon  6362  frec0g  6373  freccllem  6378  frecfcllem  6380  frecsuclem  6382  sucinc  6421  sucinc2  6422  omcl  6437  oeicl  6438  oav2  6439  omv2  6441  fvdiagfn  6667  djulclr  7022  djurclr  7023  djulcl  7024  djurcl  7025  djulclb  7028  omp1eomlem  7067  ctmlemr  7081  nnnninf  7098  nnnninfeq  7100  cardval3ex  7149  ceilqval  10249  frec2uzzd  10343  frec2uzsucd  10344  monoord2  10420  iseqf1olemqval  10430  iseqf1olemqk  10437  seq3f1olemqsum  10443  seq3f1oleml  10446  seq3f1o  10447  seq3distr  10456  ser3le  10461  hashinfom  10699  hashennn  10701  cjval  10796  reval  10800  imval  10801  cvg1nlemcau  10935  cvg1nlemres  10936  absval  10952  resqrexlemglsq  10973  resqrexlemga  10974  climmpt  11250  climle  11284  climcvg1nlem  11299  summodclem3  11330  summodclem2a  11331  zsumdc  11334  fsum3  11337  fsumcl2lem  11348  sumsnf  11359  isumadd  11381  fsumrev  11393  fsumshft  11394  fsummulc2  11398  iserabs  11425  isumlessdc  11446  divcnv  11447  trireciplem  11450  trirecip  11451  expcnvap0  11452  expcnvre  11453  expcnv  11454  explecnv  11455  geolim  11461  geolim2  11462  geo2lim  11466  geoisum  11467  geoisumr  11468  geoisum1  11469  geoisum1c  11470  cvgratz  11482  mertenslem2  11486  mertensabs  11487  fprodmul  11541  eftvalcn  11607  efval  11611  efcvgfsum  11617  ege2le3  11621  efcj  11623  eftlub  11640  efgt1p2  11645  eflegeo  11651  sinval  11652  cosval  11653  tanvalap  11658  eirraplem  11726  phival  12154  crth  12165  phimullem  12166  ennnfonelemj0  12343  ennnfonelem0  12347  strnfvnd  12423  topnvalg  12578  toponsspwpwg  12773  tgval  12802  cldval  12852  ntrfval  12853  clsfval  12854  neifval  12893  neival  12896  ismet  13097  isxmet  13098  divcnap  13308  mulc1cncf  13329  djucllem  13794  nnsf  13998  peano3nninf  14000  nninfself  14006  nninfsellemeqinf  14009  dceqnconst  14051  dcapnconst  14052