Theorem fvmptg 5722

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 2231	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2243	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2238	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2981	. . . 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 4152	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2252	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5720	. 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 1397   E*wmo 2080   e. wcel 2202   {copab 4149   |-> cmpt 4150   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334

This theorem is referenced by:  fvmpt  5723  fvmpts  5724  fvmpt3  5725  fvmpt2  5730  f1mpt  5911  caofinvl  6260  1stvalg  6304  2ndvalg  6305  brtpos2  6416  rdgon  6551  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  sucinc  6612  sucinc2  6613  omcl  6628  oeicl  6629  oav2  6630  omv2  6632  fvdiagfn  6861  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djulclb  7253  omp1eomlem  7292  ctmlemr  7306  nnnninf  7324  nnnninfeq  7326  cardval3ex  7388  ceilqval  10567  frec2uzzd  10661  frec2uzsucd  10662  monoord2  10747  iseqf1olemqval  10761  iseqf1olemqk  10768  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  seq3distr  10793  ser3le  10798  hashinfom  11039  hashennn  11041  cjval  11405  reval  11409  imval  11410  cvg1nlemcau  11544  cvg1nlemres  11545  absval  11561  resqrexlemglsq  11582  resqrexlemga  11583  climmpt  11860  climle  11894  climcvg1nlem  11909  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsum3  11947  fsumcl2lem  11958  sumsnf  11969  isumadd  11991  fsumrev  12003  fsumshft  12004  fsummulc2  12008  iserabs  12035  isumlessdc  12056  divcnv  12057  trireciplem  12060  trirecip  12061  expcnvap0  12062  expcnvre  12063  expcnv  12064  explecnv  12065  geolim  12071  geolim2  12072  geo2lim  12076  geoisum  12077  geoisumr  12078  geoisum1  12079  geoisum1c  12080  cvgratz  12092  mertenslem2  12096  mertensabs  12097  fprodmul  12151  eftvalcn  12217  efval  12221  efcvgfsum  12227  ege2le3  12231  efcj  12233  eftlub  12250  efgt1p2  12255  eflegeo  12261  sinval  12262  cosval  12263  tanvalap  12268  eirraplem  12337  phival  12784  crth  12795  phimullem  12796  ennnfonelemj0  13021  ennnfonelem0  13025  strnfvnd  13101  topnvalg  13333  tgval  13344  2idlval  14515  zrhval  14630  toponsspwpwg  14745  cldval  14822  ntrfval  14823  clsfval  14824  neifval  14863  neival  14866  ismet  15067  isxmet  15068  divcnap  15288  mulc1cncf  15312  djucllem  16396  nnsf  16607  peano3nninf  16609  nninfself  16615  nninfsellemeqinf  16618  dceqnconst  16664  dcapnconst  16665