Theorem fvmptg 5633

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 2193	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2205	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2200	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2935	. . . 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 4092	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2214	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5631	. 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 1364   E*wmo 2043   e. wcel 2164   {copab 4089   |-> cmpt 4090   ` cfv 5254

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2986  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fv 5262

This theorem is referenced by:  fvmpt  5634  fvmpts  5635  fvmpt3  5636  fvmpt2  5641  f1mpt  5814  caofinvl  6155  1stvalg  6195  2ndvalg  6196  brtpos2  6304  rdgon  6439  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  sucinc  6498  sucinc2  6499  omcl  6514  oeicl  6515  oav2  6516  omv2  6518  fvdiagfn  6747  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djulclb  7114  omp1eomlem  7153  ctmlemr  7167  nnnninf  7185  nnnninfeq  7187  cardval3ex  7245  ceilqval  10377  frec2uzzd  10471  frec2uzsucd  10472  monoord2  10557  iseqf1olemqval  10571  iseqf1olemqk  10578  seq3f1olemqsum  10584  seq3f1oleml  10587  seq3f1o  10588  seq3distr  10603  ser3le  10608  hashinfom  10849  hashennn  10851  cjval  10989  reval  10993  imval  10994  cvg1nlemcau  11128  cvg1nlemres  11129  absval  11145  resqrexlemglsq  11166  resqrexlemga  11167  climmpt  11443  climle  11477  climcvg1nlem  11492  summodclem3  11523  summodclem2a  11524  zsumdc  11527  fsum3  11530  fsumcl2lem  11541  sumsnf  11552  isumadd  11574  fsumrev  11586  fsumshft  11587  fsummulc2  11591  iserabs  11618  isumlessdc  11639  divcnv  11640  trireciplem  11643  trirecip  11644  expcnvap0  11645  expcnvre  11646  expcnv  11647  explecnv  11648  geolim  11654  geolim2  11655  geo2lim  11659  geoisum  11660  geoisumr  11661  geoisum1  11662  geoisum1c  11663  cvgratz  11675  mertenslem2  11679  mertensabs  11680  fprodmul  11734  eftvalcn  11800  efval  11804  efcvgfsum  11810  ege2le3  11814  efcj  11816  eftlub  11833  efgt1p2  11838  eflegeo  11844  sinval  11845  cosval  11846  tanvalap  11851  eirraplem  11920  phival  12351  crth  12362  phimullem  12363  ennnfonelemj0  12558  ennnfonelem0  12562  strnfvnd  12638  topnvalg  12862  tgval  12873  2idlval  13998  zrhval  14105  toponsspwpwg  14190  cldval  14267  ntrfval  14268  clsfval  14269  neifval  14308  neival  14311  ismet  14512  isxmet  14513  divcnap  14723  mulc1cncf  14744  djucllem  15292  nnsf  15495  peano3nninf  15497  nninfself  15503  nninfsellemeqinf  15506  dceqnconst  15550  dcapnconst  15551