Theorem fvmptg 5731

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 2231	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2243	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2238	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2982	. . . 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 4157	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2252	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5729	. 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 1398   E*wmo 2080   e. wcel 2202   {copab 4154   |-> cmpt 4155   ` cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341

This theorem is referenced by:  fvmpt  5732  fvmpts  5733  fvmpt3  5734  fvmpt2  5739  f1mpt  5922  caofinvl  6270  1stvalg  6314  2ndvalg  6315  brtpos2  6460  rdgon  6595  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  sucinc  6656  sucinc2  6657  omcl  6672  oeicl  6673  oav2  6674  omv2  6676  fvdiagfn  6905  djulclr  7291  djurclr  7292  djulcl  7293  djurcl  7294  djulclb  7297  omp1eomlem  7336  ctmlemr  7350  nnnninf  7368  nnnninfeq  7370  cardval3ex  7432  ceilqval  10614  frec2uzzd  10708  frec2uzsucd  10709  monoord2  10794  iseqf1olemqval  10808  iseqf1olemqk  10815  seq3f1olemqsum  10821  seq3f1oleml  10824  seq3f1o  10825  seq3distr  10840  ser3le  10845  hashinfom  11086  hashennn  11088  cjval  11468  reval  11472  imval  11473  cvg1nlemcau  11607  cvg1nlemres  11608  absval  11624  resqrexlemglsq  11645  resqrexlemga  11646  climmpt  11923  climle  11957  climcvg1nlem  11972  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsum3  12011  fsumcl2lem  12022  sumsnf  12033  isumadd  12055  fsumrev  12067  fsumshft  12068  fsummulc2  12072  iserabs  12099  isumlessdc  12120  divcnv  12121  trireciplem  12124  trirecip  12125  expcnvap0  12126  expcnvre  12127  expcnv  12128  explecnv  12129  geolim  12135  geolim2  12136  geo2lim  12140  geoisum  12141  geoisumr  12142  geoisum1  12143  geoisum1c  12144  cvgratz  12156  mertenslem2  12160  mertensabs  12161  fprodmul  12215  eftvalcn  12281  efval  12285  efcvgfsum  12291  ege2le3  12295  efcj  12297  eftlub  12314  efgt1p2  12319  eflegeo  12325  sinval  12326  cosval  12327  tanvalap  12332  eirraplem  12401  phival  12848  crth  12859  phimullem  12860  ennnfonelemj0  13085  ennnfonelem0  13089  strnfvnd  13165  topnvalg  13397  tgval  13408  2idlval  14581  zrhval  14696  toponsspwpwg  14816  cldval  14893  ntrfval  14894  clsfval  14895  neifval  14934  neival  14937  ismet  15138  isxmet  15139  divcnap  15359  mulc1cncf  15383  depindlem1  16430  djucllem  16501  nnsf  16714  peano3nninf  16716  nninfself  16722  nninfsellemeqinf  16725  dceqnconst  16776  dcapnconst  16777