Theorem fvmptg 5709

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 2229	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2241	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2236	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2978	. . . 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 4146	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2250	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5707	. 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 1395   E*wmo 2078   e. wcel 2200   {copab 4143   |-> cmpt 4144   ` cfv 5317

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-iota 5277  df-fun 5319  df-fv 5325

This theorem is referenced by:  fvmpt  5710  fvmpts  5711  fvmpt3  5712  fvmpt2  5717  f1mpt  5894  caofinvl  6242  1stvalg  6286  2ndvalg  6287  brtpos2  6395  rdgon  6530  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  sucinc  6589  sucinc2  6590  omcl  6605  oeicl  6606  oav2  6607  omv2  6609  fvdiagfn  6838  djulclr  7212  djurclr  7213  djulcl  7214  djurcl  7215  djulclb  7218  omp1eomlem  7257  ctmlemr  7271  nnnninf  7289  nnnninfeq  7291  cardval3ex  7353  ceilqval  10523  frec2uzzd  10617  frec2uzsucd  10618  monoord2  10703  iseqf1olemqval  10717  iseqf1olemqk  10724  seq3f1olemqsum  10730  seq3f1oleml  10733  seq3f1o  10734  seq3distr  10749  ser3le  10754  hashinfom  10995  hashennn  10997  cjval  11351  reval  11355  imval  11356  cvg1nlemcau  11490  cvg1nlemres  11491  absval  11507  resqrexlemglsq  11528  resqrexlemga  11529  climmpt  11806  climle  11840  climcvg1nlem  11855  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsum3  11893  fsumcl2lem  11904  sumsnf  11915  isumadd  11937  fsumrev  11949  fsumshft  11950  fsummulc2  11954  iserabs  11981  isumlessdc  12002  divcnv  12003  trireciplem  12006  trirecip  12007  expcnvap0  12008  expcnvre  12009  expcnv  12010  explecnv  12011  geolim  12017  geolim2  12018  geo2lim  12022  geoisum  12023  geoisumr  12024  geoisum1  12025  geoisum1c  12026  cvgratz  12038  mertenslem2  12042  mertensabs  12043  fprodmul  12097  eftvalcn  12163  efval  12167  efcvgfsum  12173  ege2le3  12177  efcj  12179  eftlub  12196  efgt1p2  12201  eflegeo  12207  sinval  12208  cosval  12209  tanvalap  12214  eirraplem  12283  phival  12730  crth  12741  phimullem  12742  ennnfonelemj0  12967  ennnfonelem0  12971  strnfvnd  13047  topnvalg  13279  tgval  13290  2idlval  14460  zrhval  14575  toponsspwpwg  14690  cldval  14767  ntrfval  14768  clsfval  14769  neifval  14808  neival  14811  ismet  15012  isxmet  15013  divcnap  15233  mulc1cncf  15257  djucllem  16122  nnsf  16330  peano3nninf  16332  nninfself  16338  nninfsellemeqinf  16341  dceqnconst  16387  dcapnconst  16388