Theorem fvmptg 5767

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 2438	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2449	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2444	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3130	. . . 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 4347	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2458	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5766	. 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 1369   e. wcel 1756   E*wmo 2253   {copab 4344   e. cmpt 4345   ` cfv 5413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421

This theorem is referenced by:  fvmpti  5768  fvmpt  5769  fvtresfn  5770  fvmpts  5771  fvmpt3  5772  fvmptss2  5788  f1mpt  5969  undefval  6787  tz7.44-2  6855  tz7.44-3  6856  fvdiagfn  7249  resixpfo  7293  pw2f1olem  7407  fival  7654  wdom2d  7787  cantnfp1lem1  7878  cantnfp1lem2  7879  cantnfp1lem3  7880  cantnfp1lem1OLD  7904  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  wemapwe  7920  wemapweOLD  7921  tz9.12lem3  7988  rankvalb  7996  cardval3  8114  cfval  8408  coftr  8434  fin23lem27  8489  isf34lem1  8533  fin1a2lem1  8561  fin1a2lem12  8572  axdc2lem  8609  pwcfsdom  8739  canthp1lem2  8812  wuncval  8901  tskmval  8998  lsw  12258  swrdswrd  12346  climrlim2  13017  summolem3  13183  summolem2a  13184  iserodd  13894  divsfval  14477  mreacs  14588  joinfval  15163  meetfval  15177  pwsco1mhm  15489  pwsco2mhm  15490  vrmdfval  15525  galactghm  15899  symgextfv  15914  symgextfve  15915  symgfixfvh  15932  symgfixfolem1  15935  pmtrval  15948  pmtrfv  15949  pmtrdifwrdel2lem1  15981  efgtf  16210  gsummhm2  16424  gsummhm2OLD  16425  gsummptif1n0  16445  dprdfid  16495  dprdfidOLD  16502  lspval  17033  rrgsupp  17339  aspval  17376  evlslem3  17575  coe1tmfv1  17702  coe1tmfv2  17703  ply1sclid  17715  uvcval  18185  uvcvval  18186  marepvval  18353  submaval0  18366  m2detleiblem3  18410  m2detleiblem4  18411  maduval  18419  minmar1val0  18428  tgval  18535  cldval  18602  ntrfval  18603  clsfval  18604  ntrval  18615  clsval  18616  opncldf2  18664  opncldf3  18665  neifval  18678  neival  18681  lpfval  18717  lpval  18718  1stcfb  19024  cnmpt11  19211  cnmpt21  19219  cnmptkp  19228  cnmptk1p  19233  kqfval  19271  stdbdxmet  20065  cmetcaulem  20774  bcth3  20817  iunmbl  21009  itg2gt0  21213  ellimc2  21327  cnmptlimc  21340  limccnp  21341  limcco  21343  coe1termlem  21700  coe1term  21701  ulmval  21820  pserulm  21862  rlimcnp  22334  xrlimcnp  22337  dchrelbasd  22553  nbgraf1olem4  23304  fargshiftfv  23472  grpoinvfval  23662  grpodivfval  23680  gxfval  23695  issubgo  23741  spanval  24687  nlfnval  25236  fvmpt2f  25926  sigaval  26505  measval  26564  measdivcstOLD  26590  measdivcst  26591  probfinmeasbOLD  26763  ptpcon  27074  cvmsval  27107  dfrtrclrec2  27296  rtrclreclem.refl  27297  climlec3  27352  prodmolem3  27397  prodmolem2a  27398  iprodmul  27454  bdayval  27740  imageval  27912  fvimage  27913  islocfin  28521  tailfval  28546  tailval  28547  heiborlem4  28666  heiborlem6  28668  mzpval  29021  mzpsubst  29038  rabdiophlem2  29093  fphpdo  29109  monotoddzz  29237  pw2f1o2val  29341  dnnumch3lem  29352  pwssplit4  29395  hbtlem1  29432  rgspnval  29478  refsum2cnlem1  29712  fmuldfeq  29717  stoweidlem26  29774  stoweidlem30  29778  stoweidlem31  29779  stoweidlem34  29782  stirlinglem5  29826  stirlinglem8  29829  wwlktovf1  30205  wwlktovfo  30206  wwlkn  30269  wlkiswwlksur  30304  wwlkextinj  30315  wwlkextsur  30316  clwwlkn  30383  clwwlkfv  30410  clwlkfoclwwlk  30471  clwlkf1clwwlk  30476  rusgranumwlklem1  30520  rusgranumwlklem3  30522  usg2spot2nb  30611  usgreg2spot  30613  2spotmdisj  30614  usgreghash2spot  30615  numclwlk1lem2fv  30639  numclwlk2lem2fv  30650  lincvalsc0  30844  linc0scn0  30846  linc1  30848  lincscm  30853  el0ldep  30889  bj-diagval  32372  lkrval  32573  pclvalN  33374  cdleme31fv  33874  docavalN  34608  dochval  34836  mapdval  35113  hvmapval  35245  hvmapvalvalN  35246  hdmap1vallem  35283  hdmapval  35316  hgmapval  35375