Theorem fvmptg 5948

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 2467	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2481	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2471	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3279	. . . 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 4507	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2496	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5947	. 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 1379   e. wcel 1767   E*wmo 2276   {copab 4504   |-> cmpt 4505   ` cfv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5551  df-fun 5590  df-fv 5596

This theorem is referenced by:  fvmpti  5949  fvmpt  5950  fvtresfn  5951  fvmpts  5952  fvmpt3  5953  fvmptss2  5969  f1mpt  6157  undefval  7005  tz7.44-2  7073  tz7.44-3  7074  fvdiagfn  7463  resixpfo  7507  pw2f1olem  7621  fival  7872  wdom2d  8006  cantnfp1lem1  8097  cantnfp1lem2  8098  cantnfp1lem3  8099  cantnfp1lem1OLD  8123  cantnfp1lem2OLD  8124  cantnfp1lem3OLD  8125  wemapwe  8139  wemapweOLD  8140  tz9.12lem3  8207  rankvalb  8215  cardval3  8333  cfval  8627  coftr  8653  fin23lem27  8708  isf34lem1  8752  fin1a2lem1  8780  fin1a2lem12  8791  axdc2lem  8828  pwcfsdom  8958  canthp1lem2  9031  wuncval  9120  tskmval  9217  lsw  12550  swrdswrd  12648  wwlktovf1  12858  wwlktovfo  12859  climrlim2  13333  summolem3  13499  summolem2a  13500  iserodd  14218  divsfval  14802  mreacs  14913  joinfval  15488  meetfval  15502  pwsco1mhm  15820  pwsco2mhm  15821  vrmdfval  15856  galactghm  16233  symgextfv  16248  symgextfve  16249  symgfixfvh  16266  symgfixfolem1  16269  pmtrval  16282  pmtrfv  16283  pmtrdifwrdel2lem1  16315  efgtf  16546  gsummhm2  16764  gsummhm2OLD  16765  gsummpt1n0  16795  dprdfid  16859  dprdfidOLD  16866  lspval  17421  rrgsupp  17738  aspval  17776  evlslem3  17982  coe1tmfv1  18114  coe1tmfv2  18115  ply1sclid  18128  uvcval  18611  uvcvval  18612  marepvval  18864  submaval0  18877  m2detleiblem3  18926  m2detleiblem4  18927  maduval  18935  minmar1val0  18944  tgval  19251  cldval  19318  ntrfval  19319  clsfval  19320  ntrval  19331  clsval  19332  opncldf2  19380  opncldf3  19381  neifval  19394  neival  19397  lpfval  19433  lpval  19434  1stcfb  19740  cnmpt11  19927  cnmpt21  19935  cnmptkp  19944  cnmptk1p  19949  kqfval  19987  stdbdxmet  20781  cmetcaulem  21490  bcth3  21533  iunmbl  21726  itg2gt0  21930  ellimc2  22044  cnmptlimc  22057  limccnp  22058  limcco  22060  coe1termlem  22417  coe1term  22418  ulmval  22537  pserulm  22579  rlimcnp  23051  xrlimcnp  23054  dchrelbasd  23270  nbgraf1olem4  24148  fargshiftfv  24339  wwlkn  24386  wlkiswwlksur  24423  wwlkextinj  24434  wwlkextsur  24435  clwwlkn  24471  clwwlkfv  24499  clwlkfoclwwlk  24549  clwlkf1clwwlk  24554  rusgranumwlklem1  24653  rusgranumwlklem3  24655  usg2spot2nb  24770  usgreg2spot  24772  2spotmdisj  24773  usgreghash2spot  24774  numclwlk1lem2fv  24798  numclwlk2lem2fv  24809  grpoinvfval  24930  grpodivfval  24948  gxfval  24963  issubgo  25009  spanval  25955  nlfnval  26504  fvmpt2f  27198  sigaval  27778  measval  27837  measdivcstOLD  27863  measdivcst  27864  probfinmeasbOLD  28035  ptpcon  28346  cvmsval  28379  dfrtrclrec2  28569  rtrclreclem.refl  28570  climlec3  28625  prodmolem3  28670  prodmolem2a  28671  iprodmul  28727  bdayval  29013  imageval  29185  fvimage  29186  islocfin  29796  tailfval  29821  tailval  29822  heiborlem4  29941  heiborlem6  29943  mzpval  30296  mzpsubst  30313  rabdiophlem2  30367  fphpdo  30383  monotoddzz  30511  pw2f1o2val  30613  dnnumch3lem  30624  pwssplit4  30667  hbtlem1  30704  rgspnval  30750  refsum2cnlem1  31018  fmuldfeq  31161  cncfiooicclem1  31260  stoweidlem26  31354  stoweidlem30  31358  stoweidlem31  31359  stoweidlem34  31362  stirlinglem5  31406  stirlinglem8  31409  lincvalsc0  32121  linc0scn0  32123  linc1  32125  lincscm  32130  el0ldep  32166  bj-diagval  33695  lkrval  33903  pclvalN  34704  cdleme31fv  35204  docavalN  35938  dochval  36166  mapdval  36443  hvmapval  36575  hvmapvalvalN  36576  hdmap1vallem  36613  hdmapval  36646  hgmapval  36705