Theorem fvmptg 5968

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 2461	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2471	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2465	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3225	. . . 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 4476	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2483	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5967	. 2 |- ( ( A e. D /\ C e. R ) -> ( C = C -> ( F ` A ) = C ) )
11	1, 10	mpi 20	1 |- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   e. wcel 1897   E*wmo 2310   {copab 4473   |-> cmpt 4474   ` cfv 5600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-iota 5564  df-fun 5602  df-fv 5608

This theorem is referenced by:  fvmpti  5969  fvmpt  5970  fvmpt2f  5971  fvtresfn  5972  fvmpts  5973  fvmpt3  5974  fvmptss2  5991  f1mpt  6186  undefval  7048  tz7.44-2  7150  tz7.44-3  7151  fvdiagfn  7541  resixpfo  7585  pw2f1olem  7701  fival  7951  wdom2d  8120  cantnfp1lem1  8208  cantnfp1lem2  8209  cantnfp1lem3  8210  wemapwe  8227  tz9.12lem3  8285  rankvalb  8293  cardval3  8411  cfval  8702  coftr  8728  fin23lem27  8783  isf34lem1  8827  fin1a2lem1  8855  fin1a2lem12  8866  axdc2lem  8903  pwcfsdom  9033  canthp1lem2  9103  wuncval  9192  tskmval  9289  lsw  12746  swrdswrd  12852  trclfv  13112  relexpsucnnr  13136  dfrtrclrec2  13168  rtrclreclem1  13169  climrlim2  13659  summolem3  13828  summolem2a  13829  prodmolem3  14035  prodmolem2a  14036  iprodmul  14104  iserodd  14833  divsfval  15501  mreacs  15612  joinfval  16295  meetfval  16309  pwsco1mhm  16665  pwsco2mhm  16666  vrmdfval  16688  galactghm  17092  symgextfv  17107  symgextfve  17108  symgfixfolem1  17127  pmtrval  17140  pmtrfv  17141  pmtrdifwrdel2lem1  17173  efgtf  17420  gsummhm2  17620  gsummpt1n0  17645  dprdfid  17698  lspval  18246  rrgsupp  18563  aspval  18600  evlslem3  18785  coe1tmfv1  18915  coe1tmfv2  18916  ply1sclid  18929  uvcval  19391  uvcvval  19392  marepvval  19640  submaval0  19653  m2detleiblem3  19702  m2detleiblem4  19703  maduval  19711  minmar1val0  19720  tgval  20018  cldval  20086  ntrfval  20087  clsfval  20088  ntrval  20099  clsval  20100  opncldf2  20149  opncldf3  20150  neifval  20163  neival  20166  lpfval  20202  lpval  20203  1stcfb  20508  islocfin  20580  cnmpt11  20726  cnmpt21  20734  cnmptkp  20743  cnmptk1p  20748  kqfval  20786  stdbdxmet  21578  cmetcaulem  22306  bcth3  22347  iunmbl  22554  itg2gt0  22766  ellimc2  22880  cnmptlimc  22893  limccnp  22894  limcco  22896  coe1termlem  23260  coe1term  23261  ulmval  23383  pserulm  23425  rlimcnp  23939  xrlimcnp  23942  dchrelbasd  24215  nbgraf1olem4  25220  fargshiftfv  25411  wwlkn  25458  clwwlkn  25543  clwlkfoclwwlk  25621  clwlkf1clwwlk  25626  rusgranumwlklem1  25725  usg2spot2nb  25841  usgreg2spot  25843  2spotmdisj  25844  usgreghash2spot  25845  numclwlk1lem2fv  25869  numclwlk2lem2fv  25880  grpoinvfval  26000  grpodivfval  26018  gxfval  26033  issubgo  26079  spanval  27034  nlfnval  27582  sigaval  28980  measval  29068  measdivcstOLD  29094  measdivcst  29095  probfinmeasbOLD  29309  ptpcon  30004  cvmsval  30037  climlec3  30417  bdayval  30583  imageval  30745  fvimage  30746  tailfval  31076  tailval  31077  bj-diagval  31689  heiborlem4  32190  heiborlem6  32192  lkrval  32698  pclvalN  33499  cdleme31fv  34001  docavalN  34735  dochval  34963  mapdval  35240  hvmapval  35372  hvmapvalvalN  35373  hdmap1vallem  35410  hdmapval  35443  hgmapval  35502  mzpval  35618  mzpsubst  35634  rabdiophlem2  35689  fphpdo  35704  monotoddzz  35835  pw2f1o2val  35938  dnnumch3lem  35948  pwssplit4  35991  hbtlem1  36026  rgspnval  36078  eliunov2  36315  fvmptiunrelexplb0d  36320  fvmptiunrelexplb1d  36322  refsum2cnlem1  37397  fmuldfeq  37698  cncfiooicclem1  37808  stoweidlem26  37923  stoweidlem30  37928  stoweidlem31  37929  stoweidlem34  37932  stirlinglem5  37977  stirlinglem8  37980  fourierdlem50  38057  sge0snmptf  38316  caragenval  38351  lincvalsc0  40486  linc0scn0  40488  linc1  40490  lincscm  40495  el0ldep  40531