Theorem fvmptg 5758

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 2234	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2246	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2241	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2995	. . . 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 4178	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2255	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5756	. 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 2083   e. wcel 2205   {copab 4175   |-> cmpt 4176   ` cfv 5357

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 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365

This theorem is referenced by:  fvmpt  5759  fvmpts  5760  fvmpt3  5761  fvmpt2  5766  f1mpt  5950  caofinvl  6301  1stvalg  6349  2ndvalg  6350  brtpos2  6495  rdgon  6630  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  sucinc  6691  sucinc2  6692  omcl  6707  oeicl  6708  oav2  6709  omv2  6711  fvdiagfn  6941  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djulclb  7359  omp1eomlem  7398  ctmlemr  7412  nnnninf  7430  nnnninfeq  7432  cardval3ex  7494  ceilqval  10692  frec2uzzd  10786  frec2uzsucd  10787  monoord2  10872  iseqf1olemqval  10886  iseqf1olemqk  10893  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  seq3distr  10918  ser3le  10923  hashinfom  11166  hashennn  11168  cjval  11555  reval  11559  imval  11560  cvg1nlemcau  11694  cvg1nlemres  11695  absval  11711  resqrexlemglsq  11732  resqrexlemga  11733  climmpt  12010  climle  12044  climcvg1nlem  12059  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsum3  12098  fsumcl2lem  12109  sumsnf  12120  isumadd  12142  fsumrev  12154  fsumshft  12155  fsummulc2  12159  iserabs  12186  isumlessdc  12207  divcnv  12208  trireciplem  12211  trirecip  12212  expcnvap0  12213  expcnvre  12214  expcnv  12215  explecnv  12216  geolim  12222  geolim2  12223  geo2lim  12227  geoisum  12228  geoisumr  12229  geoisum1  12230  geoisum1c  12231  cvgratz  12243  mertenslem2  12247  mertensabs  12248  fprodmul  12302  eftvalcn  12368  efval  12372  efcvgfsum  12378  ege2le3  12382  efcj  12384  eftlub  12401  efgt1p2  12406  eflegeo  12412  sinval  12413  cosval  12414  tanvalap  12419  eirraplem  12488  phival  12935  crth  12946  phimullem  12947  ennnfonelemj0  13236  ennnfonelem0  13240  strnfvnd  13316  topnvalg  13548  tgval  13559  2idlval  14776  zrhval  14891  toponsspwpwg  15013  cldval  15090  ntrfval  15091  clsfval  15092  neifval  15131  neival  15134  ismet  15335  isxmet  15336  divcnap  15556  mulc1cncf  15580  depindlem1  16627  djucllem  16698  nnsf  16909  peano3nninf  16911  nninfself  16917  nninfsellemeqinf  16920  dceqnconst  16972  dcapnconst  16973