Theorem fvmptg 5752

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 2232	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2244	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2239	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2991	. . . 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 4172	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2253	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5750	. 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 2081   e. wcel 2203   {copab 4169   |-> cmpt 4170   ` cfv 5351

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 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-mpt 4172  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359

This theorem is referenced by:  fvmpt  5753  fvmpts  5754  fvmpt3  5755  fvmpt2  5760  f1mpt  5943  caofinvl  6291  1stvalg  6335  2ndvalg  6336  brtpos2  6481  rdgon  6616  frec0g  6627  freccllem  6632  frecfcllem  6634  frecsuclem  6636  sucinc  6677  sucinc2  6678  omcl  6693  oeicl  6694  oav2  6695  omv2  6697  fvdiagfn  6927  djulclr  7339  djurclr  7340  djulcl  7341  djurcl  7342  djulclb  7345  omp1eomlem  7384  ctmlemr  7398  nnnninf  7416  nnnninfeq  7418  cardval3ex  7480  ceilqval  10667  frec2uzzd  10761  frec2uzsucd  10762  monoord2  10847  iseqf1olemqval  10861  iseqf1olemqk  10868  seq3f1olemqsum  10874  seq3f1oleml  10877  seq3f1o  10878  seq3distr  10893  ser3le  10898  hashinfom  11139  hashennn  11141  cjval  11526  reval  11530  imval  11531  cvg1nlemcau  11665  cvg1nlemres  11666  absval  11682  resqrexlemglsq  11703  resqrexlemga  11704  climmpt  11981  climle  12015  climcvg1nlem  12030  summodclem3  12062  summodclem2a  12063  zsumdc  12066  fsum3  12069  fsumcl2lem  12080  sumsnf  12091  isumadd  12113  fsumrev  12125  fsumshft  12126  fsummulc2  12130  iserabs  12157  isumlessdc  12178  divcnv  12179  trireciplem  12182  trirecip  12183  expcnvap0  12184  expcnvre  12185  expcnv  12186  explecnv  12187  geolim  12193  geolim2  12194  geo2lim  12198  geoisum  12199  geoisumr  12200  geoisum1  12201  geoisum1c  12202  cvgratz  12214  mertenslem2  12218  mertensabs  12219  fprodmul  12273  eftvalcn  12339  efval  12343  efcvgfsum  12349  ege2le3  12353  efcj  12355  eftlub  12372  efgt1p2  12377  eflegeo  12383  sinval  12384  cosval  12385  tanvalap  12390  eirraplem  12459  phival  12906  crth  12917  phimullem  12918  ennnfonelemj0  13144  ennnfonelem0  13148  strnfvnd  13224  topnvalg  13456  tgval  13467  2idlval  14642  zrhval  14757  toponsspwpwg  14879  cldval  14956  ntrfval  14957  clsfval  14958  neifval  14997  neival  15000  ismet  15201  isxmet  15202  divcnap  15422  mulc1cncf  15446  depindlem1  16493  djucllem  16564  nnsf  16775  peano3nninf  16777  nninfself  16783  nninfsellemeqinf  16786  dceqnconst  16837  dcapnconst  16838