Theorem fvmptg 5960

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 2423	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2437	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2427	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3248	. . . 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 4482	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2452	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5959	. 2 |- ( ( A e. D /\ C e. R ) -> ( C = C -> ( F ` A ) = C ) )
11	1, 10	mpi 21	1 |- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1438   e. wcel 1869   E*wmo 2267   {copab 4479   |-> cmpt 4480   ` cfv 5599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-iota 5563  df-fun 5601  df-fv 5607

This theorem is referenced by:  fvmpti  5961  fvmpt  5962  fvmpt2f  5963  fvtresfn  5964  fvmpts  5965  fvmpt3  5966  fvmptss2  5983  f1mpt  6175  undefval  7029  tz7.44-2  7131  tz7.44-3  7132  fvdiagfn  7522  resixpfo  7566  pw2f1olem  7680  fival  7930  wdom2d  8099  cantnfp1lem1  8186  cantnfp1lem2  8187  cantnfp1lem3  8188  wemapwe  8205  tz9.12lem3  8263  rankvalb  8271  cardval3  8389  cfval  8679  coftr  8705  fin23lem27  8760  isf34lem1  8804  fin1a2lem1  8832  fin1a2lem12  8843  axdc2lem  8880  pwcfsdom  9010  canthp1lem2  9080  wuncval  9169  tskmval  9266  lsw  12709  swrdswrd  12812  trclfv  13058  relexpsucnnr  13082  dfrtrclrec2  13114  rtrclreclem1  13115  climrlim2  13604  summolem3  13773  summolem2a  13774  prodmolem3  13980  prodmolem2a  13981  iprodmul  14049  iserodd  14778  divsfval  15446  mreacs  15557  joinfval  16240  meetfval  16254  pwsco1mhm  16610  pwsco2mhm  16611  vrmdfval  16633  galactghm  17037  symgextfv  17052  symgextfve  17053  symgfixfolem1  17072  pmtrval  17085  pmtrfv  17086  pmtrdifwrdel2lem1  17118  efgtf  17365  gsummhm2  17565  gsummpt1n0  17590  dprdfid  17643  lspval  18191  rrgsupp  18508  aspval  18545  evlslem3  18730  coe1tmfv1  18860  coe1tmfv2  18861  ply1sclid  18874  uvcval  19335  uvcvval  19336  marepvval  19584  submaval0  19597  m2detleiblem3  19646  m2detleiblem4  19647  maduval  19655  minmar1val0  19664  tgval  19962  cldval  20030  ntrfval  20031  clsfval  20032  ntrval  20043  clsval  20044  opncldf2  20093  opncldf3  20094  neifval  20107  neival  20110  lpfval  20146  lpval  20147  1stcfb  20452  islocfin  20524  cnmpt11  20670  cnmpt21  20678  cnmptkp  20687  cnmptk1p  20692  kqfval  20730  stdbdxmet  21522  cmetcaulem  22250  bcth3  22291  iunmbl  22498  itg2gt0  22710  ellimc2  22824  cnmptlimc  22837  limccnp  22838  limcco  22840  coe1termlem  23204  coe1term  23205  ulmval  23327  pserulm  23369  rlimcnp  23883  xrlimcnp  23886  dchrelbasd  24159  nbgraf1olem4  25164  fargshiftfv  25355  wwlkn  25402  clwwlkn  25487  clwlkfoclwwlk  25565  clwlkf1clwwlk  25570  rusgranumwlklem1  25669  usg2spot2nb  25785  usgreg2spot  25787  2spotmdisj  25788  usgreghash2spot  25789  numclwlk1lem2fv  25813  numclwlk2lem2fv  25824  grpoinvfval  25944  grpodivfval  25962  gxfval  25977  issubgo  26023  spanval  26978  nlfnval  27526  sigaval  28934  measval  29022  measdivcstOLD  29048  measdivcst  29049  probfinmeasbOLD  29263  ptpcon  29958  cvmsval  29991  climlec3  30370  bdayval  30536  imageval  30696  fvimage  30697  tailfval  31027  tailval  31028  bj-diagval  31603  heiborlem4  32066  heiborlem6  32068  lkrval  32579  pclvalN  33380  cdleme31fv  33882  docavalN  34616  dochval  34844  mapdval  35121  hvmapval  35253  hvmapvalvalN  35254  hdmap1vallem  35291  hdmapval  35324  hgmapval  35383  mzpval  35499  mzpsubst  35515  rabdiophlem2  35570  fphpdo  35585  monotoddzz  35717  pw2f1o2val  35820  dnnumch3lem  35830  pwssplit4  35873  hbtlem1  35908  rgspnval  35960  eliunov2  36137  fvmptiunrelexplb0d  36142  fvmptiunrelexplb1d  36144  refsum2cnlem1  37225  fmuldfeq  37487  cncfiooicclem1  37597  stoweidlem26  37712  stoweidlem30  37717  stoweidlem31  37718  stoweidlem34  37721  stirlinglem5  37766  stirlinglem8  37769  fourierdlem50  37846  salgenval  37989  caragenval  38099  lincvalsc0  39520  linc0scn0  39522  linc1  39524  lincscm  39529  el0ldep  39565