Theorem fvmptg 5718

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 2979	. . . 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 4150	. . . 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 5716	. 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 4147   |-> cmpt 4148   ` cfv 5324

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332

This theorem is referenced by:  fvmpt  5719  fvmpts  5720  fvmpt3  5721  fvmpt2  5726  f1mpt  5907  caofinvl  6256  1stvalg  6300  2ndvalg  6301  brtpos2  6412  rdgon  6547  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  sucinc  6608  sucinc2  6609  omcl  6624  oeicl  6625  oav2  6626  omv2  6628  fvdiagfn  6857  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djulclb  7245  omp1eomlem  7284  ctmlemr  7298  nnnninf  7316  nnnninfeq  7318  cardval3ex  7380  ceilqval  10558  frec2uzzd  10652  frec2uzsucd  10653  monoord2  10738  iseqf1olemqval  10752  iseqf1olemqk  10759  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  seq3distr  10784  ser3le  10789  hashinfom  11030  hashennn  11032  cjval  11396  reval  11400  imval  11401  cvg1nlemcau  11535  cvg1nlemres  11536  absval  11552  resqrexlemglsq  11573  resqrexlemga  11574  climmpt  11851  climle  11885  climcvg1nlem  11900  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsum3  11938  fsumcl2lem  11949  sumsnf  11960  isumadd  11982  fsumrev  11994  fsumshft  11995  fsummulc2  11999  iserabs  12026  isumlessdc  12047  divcnv  12048  trireciplem  12051  trirecip  12052  expcnvap0  12053  expcnvre  12054  expcnv  12055  explecnv  12056  geolim  12062  geolim2  12063  geo2lim  12067  geoisum  12068  geoisumr  12069  geoisum1  12070  geoisum1c  12071  cvgratz  12083  mertenslem2  12087  mertensabs  12088  fprodmul  12142  eftvalcn  12208  efval  12212  efcvgfsum  12218  ege2le3  12222  efcj  12224  eftlub  12241  efgt1p2  12246  eflegeo  12252  sinval  12253  cosval  12254  tanvalap  12259  eirraplem  12328  phival  12775  crth  12786  phimullem  12787  ennnfonelemj0  13012  ennnfonelem0  13016  strnfvnd  13092  topnvalg  13324  tgval  13335  2idlval  14506  zrhval  14621  toponsspwpwg  14736  cldval  14813  ntrfval  14814  clsfval  14815  neifval  14854  neival  14857  ismet  15058  isxmet  15059  divcnap  15279  mulc1cncf  15303  djucllem  16332  nnsf  16543  peano3nninf  16545  nninfself  16551  nninfsellemeqinf  16554  dceqnconst  16600  dcapnconst  16601