Theorem fvmptg 5760

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 2433	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2444	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2439	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3124	. . . 4 |- E* y y = B
6	5	a1i 11	. . 3 |- ( x e. D -> E* y y = B )
7		fvmptg.2	. . . 4 |- F = ( x e. D |-> B )
8		df-mpt 4340	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2453	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5759	. 2 |- ( ( A e. D /\ C e. R ) -> ( C = C -> ( F ` A ) = C ) )
11	1, 10	mpi 17	1 |- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   E*wmo 2255   {copab 4337   e. cmpt 4338   ` cfv 5406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fv 5414

This theorem is referenced by:  fvmpti  5761  fvmpt  5762  fvtresfn  5763  fvmpts  5764  fvmpt3  5765  fvmptss2  5781  f1mpt  5961  undefval  6781  tz7.44-2  6849  tz7.44-3  6850  fvdiagfn  7245  resixpfo  7289  pw2f1olem  7403  fival  7650  wdom2d  7783  cantnfp1lem1  7874  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnfp1lem1OLD  7900  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  wemapwe  7916  wemapweOLD  7917  tz9.12lem3  7984  rankvalb  7992  cardval3  8110  cfval  8404  coftr  8430  fin23lem27  8485  isf34lem1  8529  fin1a2lem1  8557  fin1a2lem12  8568  axdc2lem  8605  pwcfsdom  8735  canthp1lem2  8808  wuncval  8897  tskmval  8994  lsw  12250  swrdswrd  12338  climrlim2  13009  summolem3  13175  summolem2a  13176  iserodd  13885  divsfval  14468  mreacs  14579  joinfval  15154  meetfval  15168  pwsco1mhm  15480  pwsco2mhm  15481  vrmdfval  15514  galactghm  15888  symgextfv  15903  symgextfve  15904  symgfixfvh  15921  symgfixfolem1  15924  pmtrval  15937  pmtrfv  15938  pmtrdifwrdel2lem1  15970  efgtf  16199  gsummhm2  16411  gsummhm2OLD  16412  gsummptif1n0  16431  dprdfid  16481  dprdfidOLD  16488  lspval  16978  rrgsupp  17284  aspval  17321  coe1tmfv1  17625  coe1tmfv2  17626  ply1sclid  17638  uvcval  18052  uvcvval  18053  marepvval  18220  submaval0  18233  m2detleiblem3  18277  m2detleiblem4  18278  maduval  18286  minmar1val0  18295  tgval  18402  cldval  18469  ntrfval  18470  clsfval  18471  ntrval  18482  clsval  18483  opncldf2  18531  opncldf3  18532  neifval  18545  neival  18548  lpfval  18584  lpval  18585  1stcfb  18891  cnmpt11  19078  cnmpt21  19086  cnmptkp  19095  cnmptk1p  19100  kqfval  19138  stdbdxmet  19932  cmetcaulem  20641  bcth3  20684  iunmbl  20876  itg2gt0  21080  ellimc2  21194  cnmptlimc  21207  limccnp  21208  limcco  21210  evlslem3  21366  coe1termlem  21610  coe1term  21611  ulmval  21730  pserulm  21772  rlimcnp  22244  xrlimcnp  22247  dchrelbasd  22463  nbgraf1olem4  23176  fargshiftfv  23344  grpoinvfval  23534  grpodivfval  23552  gxfval  23567  issubgo  23613  spanval  24559  nlfnval  25108  fvmpt2f  25799  sigaval  26407  measval  26466  measdivcstOLD  26492  measdivcst  26493  probfinmeasbOLD  26659  ptpcon  26970  cvmsval  27003  dfrtrclrec2  27192  rtrclreclem.refl  27193  climlec3  27248  prodmolem3  27293  prodmolem2a  27294  iprodmul  27350  bdayval  27636  imageval  27808  fvimage  27809  islocfin  28412  tailfval  28437  tailval  28438  heiborlem4  28557  heiborlem6  28559  mzpval  28913  mzpsubst  28930  rabdiophlem2  28985  fphpdo  29001  monotoddzz  29129  pw2f1o2val  29233  dnnumch3lem  29244  pwssplit4  29287  hbtlem1  29324  rgspnval  29370  refsum2cnlem1  29604  fmuldfeq  29609  stoweidlem26  29667  stoweidlem30  29671  stoweidlem31  29672  stoweidlem34  29675  stirlinglem5  29719  stirlinglem8  29722  wwlktovf1  30098  wwlktovfo  30099  wwlkn  30162  wlkiswwlksur  30197  wwlkextinj  30208  wwlkextsur  30209  clwwlkn  30276  clwwlkfv  30303  clwlkfoclwwlk  30364  clwlkf1clwwlk  30369  rusgranumwlklem1  30413  rusgranumwlklem3  30415  usg2spot2nb  30504  usgreg2spot  30506  2spotmdisj  30507  usgreghash2spot  30508  numclwlk1lem2fv  30532  numclwlk2lem2fv  30543  lincvalsc0  30685  linc0scn0  30687  linc1  30689  lincscm  30694  el0ldep  30730  bj-diagval  32126  lkrval  32327  pclvalN  33128  cdleme31fv  33628  docavalN  34362  dochval  34590  mapdval  34867  hvmapval  34999  hvmapvalvalN  35000  hdmap1vallem  35037  hdmapval  35070  hgmapval  35129