Theorem fvmptg 5556

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 2164	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2176	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2171	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2896	. . . 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 4039	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2185	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5554	. 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 1342   E*wmo 2014   e. wcel 2135   {copab 4036   |-> cmpt 4037   ` cfv 5182

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-sbc 2947  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-mpt 4039  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-iota 5147  df-fun 5184  df-fv 5190

This theorem is referenced by:  fvmpt  5557  fvmpts  5558  fvmpt3  5559  fvmpt2  5563  f1mpt  5733  caofinvl  6066  1stvalg  6102  2ndvalg  6103  brtpos2  6210  rdgon  6345  frec0g  6356  freccllem  6361  frecfcllem  6363  frecsuclem  6365  sucinc  6404  sucinc2  6405  omcl  6420  oeicl  6421  oav2  6422  omv2  6424  fvdiagfn  6650  djulclr  7005  djurclr  7006  djulcl  7007  djurcl  7008  djulclb  7011  omp1eomlem  7050  ctmlemr  7064  nnnninf  7081  nnnninfeq  7083  cardval3ex  7132  ceilqval  10231  frec2uzzd  10325  frec2uzsucd  10326  monoord2  10402  iseqf1olemqval  10412  iseqf1olemqk  10419  seq3f1olemqsum  10425  seq3f1oleml  10428  seq3f1o  10429  seq3distr  10438  ser3le  10443  hashinfom  10680  hashennn  10682  cjval  10773  reval  10777  imval  10778  cvg1nlemcau  10912  cvg1nlemres  10913  absval  10929  resqrexlemglsq  10950  resqrexlemga  10951  climmpt  11227  climle  11261  climcvg1nlem  11276  summodclem3  11307  summodclem2a  11308  zsumdc  11311  fsum3  11314  fsumcl2lem  11325  sumsnf  11336  isumadd  11358  fsumrev  11370  fsumshft  11371  fsummulc2  11375  iserabs  11402  isumlessdc  11423  divcnv  11424  trireciplem  11427  trirecip  11428  expcnvap0  11429  expcnvre  11430  expcnv  11431  explecnv  11432  geolim  11438  geolim2  11439  geo2lim  11443  geoisum  11444  geoisumr  11445  geoisum1  11446  geoisum1c  11447  cvgratz  11459  mertenslem2  11463  mertensabs  11464  fprodmul  11518  eftvalcn  11584  efval  11588  efcvgfsum  11594  ege2le3  11598  efcj  11600  eftlub  11617  efgt1p2  11622  eflegeo  11628  sinval  11629  cosval  11630  tanvalap  11635  eirraplem  11703  phival  12122  crth  12133  phimullem  12134  ennnfonelemj0  12271  ennnfonelem0  12275  strnfvnd  12351  topnvalg  12504  toponsspwpwg  12561  tgval  12590  cldval  12640  ntrfval  12641  clsfval  12642  neifval  12681  neival  12684  ismet  12885  isxmet  12886  divcnap  13096  mulc1cncf  13117  djucllem  13516  nnsf  13719  peano3nninf  13721  nninfself  13727  nninfsellemeqinf  13730  dceqnconst  13772  dcapnconst  13773