Theorem fvmptg 6280

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 2622	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2632	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2626	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3382	. . . 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 4730	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2644	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 6278	. 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 384   = wceq 1483   e. wcel 1990   E*wmo 2471   {copab 4712   |-> cmpt 4729   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896

This theorem is referenced by:  fvmpti  6281  fvmpt  6282  fvmpt2f  6283  fvtresfn  6284  fvmpts  6285  fvmpt3  6286  fvmptss2  6304  f1mpt  6518  undefval  7402  tz7.44-2  7503  tz7.44-3  7504  fvdiagfn  7902  resixpfo  7946  pw2f1olem  8064  fival  8318  wdom2d  8485  cantnfp1lem1  8575  cantnfp1lem2  8576  cantnfp1lem3  8577  wemapwe  8594  tz9.12lem3  8652  rankvalb  8660  cardval3  8778  cfval  9069  coftr  9095  fin23lem27  9150  isf34lem1  9194  fin1a2lem1  9222  fin1a2lem12  9233  axdc2lem  9270  pwcfsdom  9405  canthp1lem2  9475  wuncval  9564  tskmval  9661  lsw  13351  swrdswrd  13460  trclfv  13741  relexpsucnnr  13765  dfrtrclrec2  13797  rtrclreclem1  13798  climrlim2  14278  summolem3  14445  summolem2a  14446  prodmolem3  14663  prodmolem2a  14664  iprodmul  14734  iserodd  15540  divsfval  16207  mreacs  16319  joinfval  17001  meetfval  17015  pwsco1mhm  17370  pwsco2mhm  17371  vrmdfval  17393  galactghm  17823  symgextfv  17838  symgextfve  17839  symgfixfolem1  17858  pmtrval  17871  pmtrfv  17872  pmtrdifwrdel2lem1  17904  efgtf  18135  gsummhm2  18339  gsummpt1n0  18364  dprdfid  18416  lspval  18975  rrgsupp  19291  aspval  19328  evlslem3  19514  coe1tmfv1  19644  coe1tmfv2  19645  ply1sclid  19658  uvcval  20124  uvcvval  20125  marepvval  20373  submaval0  20386  m2detleiblem3  20435  m2detleiblem4  20436  maduval  20444  minmar1val0  20453  toponsspwpw  20726  tgval  20759  cldval  20827  ntrfval  20828  clsfval  20829  ntrval  20840  clsval  20841  opncldf2  20889  opncldf3  20890  neifval  20903  neival  20906  lpfval  20942  lpval  20943  1stcfb  21248  islocfin  21320  cnmpt11  21466  cnmpt21  21474  cnmptkp  21483  cnmptk1p  21488  kqfval  21526  stdbdxmet  22320  cmetcaulem  23086  bcth3  23128  iunmbl  23321  itg2gt0  23527  ellimc2  23641  cnmptlimc  23654  limccnp  23655  limcco  23657  coe1termlem  24014  coe1term  24015  ulmval  24134  pserulm  24176  rlimcnp  24692  xrlimcnp  24695  dchrelbasd  24964  clwlksfoclwwlk  26963  clwlksf1clwwlk  26969  grpoinvfval  27376  grpodivfval  27388  spanval  28192  nlfnval  28740  sigaval  30173  measval  30261  measdivcstOLD  30287  measdivcst  30288  probfinmeasbOLD  30490  ptpconn  31215  cvmsval  31248  climlec3  31619  bdayval  31801  madeval  31935  imageval  32037  fvimage  32038  tailfval  32367  tailval  32368  bj-diagval  33090  curfv  33389  heiborlem4  33613  heiborlem6  33615  lkrval  34375  pclvalN  35176  cdleme31fv  35678  docavalN  36412  dochval  36640  mapdval  36917  hvmapval  37049  hvmapvalvalN  37050  hdmap1vallem  37087  hdmapval  37120  hgmapval  37179  mzpval  37295  mzpsubst  37311  rabdiophlem2  37366  fphpdo  37381  monotoddzz  37508  pw2f1o2val  37606  dnnumch3lem  37616  pwssplit4  37659  hbtlem1  37693  rgspnval  37738  eliunov2  37971  fvmptiunrelexplb0d  37976  fvmptiunrelexplb1d  37978  refsum2cnlem1  39196  fmuldfeq  39815  cncfiooicclem1  40106  stoweidlem26  40243  stoweidlem30  40247  stoweidlem31  40248  stoweidlem34  40251  stirlinglem5  40295  stirlinglem8  40298  fourierdlem50  40373  sge0snmptf  40654  caragenval  40707  fargshiftfv  41375  lincvalsc0  42210  linc0scn0  42212  linc1  42214  lincscm  42219  el0ldep  42255