Theorem fvmptg 5763

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 2404	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2415	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2410	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3070	. . . 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 4228	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2424	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5762	. 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 359   = wceq 1649   e. wcel 1721   E*wmo 2255   {copab 4225   e. cmpt 4226   ` cfv 5413

This theorem is referenced by:  fvmpti  5764  fvmpt  5765  fvmpts  5766  fvmpt3  5767  fvmptss2  5783  f1mpt  5966  undefval  6505  tz7.44-2  6624  tz7.44-3  6625  fvdiagfn  7017  resixpfo  7059  pw2f1olem  7171  fival  7375  wdom2d  7504  cantnfp1lem1  7590  cantnfp1lem2  7591  cantnfp1lem3  7592  wemapwe  7610  tz9.12lem3  7671  rankvalb  7679  cardval3  7795  cfval  8083  coftr  8109  fin23lem27  8164  isf34lem1  8208  fin1a2lem1  8236  fin1a2lem12  8247  axdc2lem  8284  pwcfsdom  8414  canthp1lem2  8484  wuncval  8573  tskmval  8670  climrlim2  12296  summolem3  12463  summolem2a  12464  iserodd  13164  divsfval  13727  mreacs  13838  pwsco1mhm  14724  pwsco2mhm  14725  vrmdfval  14756  galactghm  15061  efgtf  15309  gsummhm2  15490  dprdfid  15530  lspval  16006  aspval  16342  coe1tmfv1  16621  coe1tmfv2  16622  ply1sclid  16634  tgval  16975  cldval  17042  ntrfval  17043  clsfval  17044  ntrval  17055  clsval  17056  opncldf2  17104  opncldf3  17105  neifval  17118  neival  17121  lpfval  17157  lpval  17158  1stcfb  17461  cnmpt11  17648  cnmpt21  17656  cnmptkp  17665  cnmptk1p  17670  kqfval  17708  stdbdxmet  18498  cmetcaulem  19194  bcth3  19237  iunmbl  19400  itg2gt0  19605  ellimc2  19717  cnmptlimc  19730  limccnp  19731  limcco  19733  evlslem3  19888  coe1termlem  20129  coe1term  20130  ulmval  20249  pserulm  20291  rlimcnp  20757  xrlimcnp  20760  dchrelbasd  20976  nbgraf1olem4  21407  fargshiftfv  21575  grpoinvfval  21765  grpodivfval  21783  gxfval  21798  issubgo  21844  spanval  22788  nlfnval  23337  fvmpt2f  24025  sigaval  24446  measval  24505  measdivcstOLD  24531  measdivcst  24532  probfinmeasbOLD  24639  ptpcon  24873  cvmsval  24906  dfrtrclrec2  25096  rtrclreclem.refl  25097  climlec3  25167  prodmolem3  25212  prodmolem2a  25213  iprodmul  25269  bdayval  25516  imageval  25683  fvimage  25684  islocfin  26266  tailfval  26291  tailval  26292  heiborlem4  26413  heiborlem6  26415  fvtresfn  26634  mzpval  26679  mzpsubst  26695  rabdiophlem2  26752  fphpdo  26768  monotoddzz  26896  pw2f1o2val  27000  dnnumch3lem  27011  pwssplit4  27059  uvcval  27102  uvcvval  27103  hbtlem1  27195  rgspnval  27241  pmtrval  27262  pmtrfv  27263  refsum2cnlem1  27575  fmuldfeq  27580  stoweidlem26  27642  stoweidlem30  27646  stoweidlem31  27647  stoweidlem34  27650  stirlinglem5  27694  stirlinglem8  27697  swrdswrd  28011  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  usgreghash2spot  28172  lkrval  29571  pclvalN  30372  cdleme31fv  30872  docavalN  31606  dochval  31834  mapdval  32111  hvmapval  32243  hvmapvalvalN  32244  hdmap1vallem  32281  hdmapval  32314  hgmapval  32373

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421