Theorem fvmptg 5929

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 2454	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2468	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2458	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3272	. . . 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 4499	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2483	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5928	. 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 367   = wceq 1398   e. wcel 1823   E*wmo 2285   {copab 4496   |-> cmpt 4497   ` cfv 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fv 5578

This theorem is referenced by:  fvmpti  5930  fvmpt  5931  fvtresfn  5932  fvmpts  5933  fvmpt3  5934  fvmptss2  5951  f1mpt  6144  undefval  6997  tz7.44-2  7065  tz7.44-3  7066  fvdiagfn  7456  resixpfo  7500  pw2f1olem  7614  fival  7864  wdom2d  7998  cantnfp1lem1  8088  cantnfp1lem2  8089  cantnfp1lem3  8090  cantnfp1lem1OLD  8114  cantnfp1lem2OLD  8115  cantnfp1lem3OLD  8116  wemapwe  8130  wemapweOLD  8131  tz9.12lem3  8198  rankvalb  8206  cardval3  8324  cfval  8618  coftr  8644  fin23lem27  8699  isf34lem1  8743  fin1a2lem1  8771  fin1a2lem12  8782  axdc2lem  8819  pwcfsdom  8949  canthp1lem2  9020  wuncval  9109  tskmval  9206  lsw  12573  swrdswrd  12676  trclfv  12918  relexpsucnnr  12942  dfrtrclrec2  12972  rtrclreclem1  12973  climrlim2  13452  summolem3  13618  summolem2a  13619  prodmolem3  13822  prodmolem2a  13823  iprodmul  13878  iserodd  14443  divsfval  15036  mreacs  15147  joinfval  15830  meetfval  15844  pwsco1mhm  16200  pwsco2mhm  16201  vrmdfval  16223  galactghm  16627  symgextfv  16642  symgextfve  16643  symgfixfolem1  16662  pmtrval  16675  pmtrfv  16676  pmtrdifwrdel2lem1  16708  efgtf  16939  gsummhm2  17159  gsummhm2OLD  17160  gsummpt1n0  17188  dprdfid  17252  dprdfidOLD  17259  lspval  17816  rrgsupp  18134  aspval  18172  evlslem3  18378  coe1tmfv1  18510  coe1tmfv2  18511  ply1sclid  18524  uvcval  18987  uvcvval  18988  marepvval  19236  submaval0  19249  m2detleiblem3  19298  m2detleiblem4  19299  maduval  19307  minmar1val0  19316  tgval  19623  cldval  19691  ntrfval  19692  clsfval  19693  ntrval  19704  clsval  19705  opncldf2  19753  opncldf3  19754  neifval  19767  neival  19770  lpfval  19806  lpval  19807  1stcfb  20112  islocfin  20184  cnmpt11  20330  cnmpt21  20338  cnmptkp  20347  cnmptk1p  20352  kqfval  20390  stdbdxmet  21184  cmetcaulem  21893  bcth3  21936  iunmbl  22129  itg2gt0  22333  ellimc2  22447  cnmptlimc  22460  limccnp  22461  limcco  22463  coe1termlem  22821  coe1term  22822  ulmval  22941  pserulm  22983  rlimcnp  23493  xrlimcnp  23496  dchrelbasd  23712  nbgraf1olem4  24646  fargshiftfv  24837  wwlkn  24884  clwwlkn  24969  clwlkfoclwwlk  25047  clwlkf1clwwlk  25052  rusgranumwlklem1  25151  usg2spot2nb  25267  usgreg2spot  25269  2spotmdisj  25270  usgreghash2spot  25271  numclwlk1lem2fv  25295  numclwlk2lem2fv  25306  grpoinvfval  25424  grpodivfval  25442  gxfval  25457  issubgo  25503  spanval  26449  nlfnval  26998  fvmpt2f  27720  sigaval  28340  measval  28406  measdivcstOLD  28432  measdivcst  28433  probfinmeasbOLD  28631  ptpcon  28942  cvmsval  28975  climlec3  29361  bdayval  29648  imageval  29808  fvimage  29809  tailfval  30430  tailval  30431  heiborlem4  30550  heiborlem6  30552  mzpval  30904  mzpsubst  30920  rabdiophlem2  30975  fphpdo  30990  monotoddzz  31118  pw2f1o2val  31220  dnnumch3lem  31231  pwssplit4  31274  hbtlem1  31313  rgspnval  31358  refsum2cnlem1  31652  fmuldfeq  31816  cncfiooicclem1  31935  stoweidlem26  32047  stoweidlem30  32051  stoweidlem31  32052  stoweidlem34  32055  stirlinglem5  32099  stirlinglem8  32102  fourierdlem50  32178  lincvalsc0  33276  linc0scn0  33278  linc1  33280  lincscm  33285  el0ldep  33321  bj-diagval  35006  lkrval  35210  pclvalN  36011  cdleme31fv  36513  docavalN  37247  dochval  37475  mapdval  37752  hvmapval  37884  hvmapvalvalN  37885  hdmap1vallem  37922  hdmapval  37955  hgmapval  38014  eliunov2  38200