Theorem fvmptg 5935

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 2441	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2455	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2445	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3259	. . . 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 4493	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2470	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5934	. 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 1381   e. wcel 1802   E*wmo 2267   {copab 4490   |-> cmpt 4491   ` cfv 5574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-iota 5537  df-fun 5576  df-fv 5582

This theorem is referenced by:  fvmpti  5936  fvmpt  5937  fvtresfn  5938  fvmpts  5939  fvmpt3  5940  fvmptss2  5956  f1mpt  6150  undefval  7003  tz7.44-2  7071  tz7.44-3  7072  fvdiagfn  7461  resixpfo  7505  pw2f1olem  7619  fival  7870  wdom2d  8004  cantnfp1lem1  8095  cantnfp1lem2  8096  cantnfp1lem3  8097  cantnfp1lem1OLD  8121  cantnfp1lem2OLD  8122  cantnfp1lem3OLD  8123  wemapwe  8137  wemapweOLD  8138  tz9.12lem3  8205  rankvalb  8213  cardval3  8331  cfval  8625  coftr  8651  fin23lem27  8706  isf34lem1  8750  fin1a2lem1  8778  fin1a2lem12  8789  axdc2lem  8826  pwcfsdom  8956  canthp1lem2  9029  wuncval  9118  tskmval  9215  lsw  12559  swrdswrd  12659  climrlim2  13344  summolem3  13510  summolem2a  13511  iserodd  14231  divsfval  14816  mreacs  14927  joinfval  15500  meetfval  15514  pwsco1mhm  15870  pwsco2mhm  15871  vrmdfval  15893  galactghm  16297  symgextfv  16312  symgextfve  16313  symgfixfolem1  16332  pmtrval  16345  pmtrfv  16346  pmtrdifwrdel2lem1  16378  efgtf  16609  gsummhm2  16830  gsummhm2OLD  16831  gsummpt1n0  16861  dprdfid  16925  dprdfidOLD  16932  lspval  17489  rrgsupp  17807  aspval  17845  evlslem3  18051  coe1tmfv1  18183  coe1tmfv2  18184  ply1sclid  18197  uvcval  18683  uvcvval  18684  marepvval  18936  submaval0  18949  m2detleiblem3  18998  m2detleiblem4  18999  maduval  19007  minmar1val0  19016  tgval  19323  cldval  19390  ntrfval  19391  clsfval  19392  ntrval  19403  clsval  19404  opncldf2  19452  opncldf3  19453  neifval  19466  neival  19469  lpfval  19505  lpval  19506  1stcfb  19812  islocfin  19884  cnmpt11  20030  cnmpt21  20038  cnmptkp  20047  cnmptk1p  20052  kqfval  20090  stdbdxmet  20884  cmetcaulem  21593  bcth3  21636  iunmbl  21829  itg2gt0  22033  ellimc2  22147  cnmptlimc  22160  limccnp  22161  limcco  22163  coe1termlem  22520  coe1term  22521  ulmval  22640  pserulm  22682  rlimcnp  23160  xrlimcnp  23163  dchrelbasd  23379  nbgraf1olem4  24309  fargshiftfv  24500  wwlkn  24547  clwwlkn  24632  clwlkfoclwwlk  24710  clwlkf1clwwlk  24715  rusgranumwlklem1  24814  usg2spot2nb  24930  usgreg2spot  24932  2spotmdisj  24933  usgreghash2spot  24934  numclwlk1lem2fv  24958  numclwlk2lem2fv  24969  grpoinvfval  25091  grpodivfval  25109  gxfval  25124  issubgo  25170  spanval  26116  nlfnval  26665  fvmpt2f  27363  sigaval  27976  measval  28035  measdivcstOLD  28061  measdivcst  28062  probfinmeasbOLD  28233  ptpcon  28544  cvmsval  28577  dfrtrclrec2  28932  rtrclreclem.refl  28933  climlec3  28988  prodmolem3  29033  prodmolem2a  29034  iprodmul  29090  bdayval  29376  imageval  29548  fvimage  29549  tailfval  30158  tailval  30159  heiborlem4  30278  heiborlem6  30280  mzpval  30632  mzpsubst  30649  rabdiophlem2  30703  fphpdo  30719  monotoddzz  30847  pw2f1o2val  30949  dnnumch3lem  30960  pwssplit4  31003  hbtlem1  31040  rgspnval  31086  refsum2cnlem1  31359  fmuldfeq  31501  cncfiooicclem1  31599  stoweidlem26  31693  stoweidlem30  31697  stoweidlem31  31698  stoweidlem34  31701  stirlinglem5  31745  stirlinglem8  31748  fourierdlem50  31824  lincvalsc0  32732  linc0scn0  32734  linc1  32736  lincscm  32741  el0ldep  32777  bj-diagval  34308  lkrval  34515  pclvalN  35316  cdleme31fv  35818  docavalN  36552  dochval  36780  mapdval  37057  hvmapval  37189  hvmapvalvalN  37190  hdmap1vallem  37227  hdmapval  37260  hgmapval  37319