Theorem fvmptg 5880

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 3240	. . . 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 4459	. . . 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 5879	. 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 1370   e. wcel 1758   E*wmo 2263   {copab 4456   |-> cmpt 4457   ` cfv 5525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-iota 5488  df-fun 5527  df-fv 5533

This theorem is referenced by:  fvmpti  5881  fvmpt  5882  fvtresfn  5883  fvmpts  5884  fvmpt3  5885  fvmptss2  5901  f1mpt  6082  undefval  6904  tz7.44-2  6972  tz7.44-3  6973  fvdiagfn  7366  resixpfo  7410  pw2f1olem  7524  fival  7772  wdom2d  7905  cantnfp1lem1  7996  cantnfp1lem2  7997  cantnfp1lem3  7998  cantnfp1lem1OLD  8022  cantnfp1lem2OLD  8023  cantnfp1lem3OLD  8024  wemapwe  8038  wemapweOLD  8039  tz9.12lem3  8106  rankvalb  8114  cardval3  8232  cfval  8526  coftr  8552  fin23lem27  8607  isf34lem1  8651  fin1a2lem1  8679  fin1a2lem12  8690  axdc2lem  8727  pwcfsdom  8857  canthp1lem2  8930  wuncval  9019  tskmval  9116  lsw  12383  swrdswrd  12471  climrlim2  13142  summolem3  13308  summolem2a  13309  iserodd  14019  divsfval  14603  mreacs  14714  joinfval  15289  meetfval  15303  pwsco1mhm  15616  pwsco2mhm  15617  vrmdfval  15652  galactghm  16026  symgextfv  16041  symgextfve  16042  symgfixfvh  16059  symgfixfolem1  16062  pmtrval  16075  pmtrfv  16076  pmtrdifwrdel2lem1  16108  efgtf  16339  gsummhm2  16555  gsummhm2OLD  16556  gsummpt1n0  16577  dprdfid  16628  dprdfidOLD  16635  lspval  17178  rrgsupp  17484  aspval  17521  evlslem3  17723  coe1tmfv1  17850  coe1tmfv2  17851  ply1sclid  17864  uvcval  18334  uvcvval  18335  marepvval  18504  submaval0  18517  m2detleiblem3  18566  m2detleiblem4  18567  maduval  18575  minmar1val0  18584  tgval  18691  cldval  18758  ntrfval  18759  clsfval  18760  ntrval  18771  clsval  18772  opncldf2  18820  opncldf3  18821  neifval  18834  neival  18837  lpfval  18873  lpval  18874  1stcfb  19180  cnmpt11  19367  cnmpt21  19375  cnmptkp  19384  cnmptk1p  19389  kqfval  19427  stdbdxmet  20221  cmetcaulem  20930  bcth3  20973  iunmbl  21166  itg2gt0  21370  ellimc2  21484  cnmptlimc  21497  limccnp  21498  limcco  21500  coe1termlem  21857  coe1term  21858  ulmval  21977  pserulm  22019  rlimcnp  22491  xrlimcnp  22494  dchrelbasd  22710  nbgraf1olem4  23504  fargshiftfv  23672  grpoinvfval  23862  grpodivfval  23880  gxfval  23895  issubgo  23941  spanval  24887  nlfnval  25436  fvmpt2f  26125  sigaval  26697  measval  26756  measdivcstOLD  26782  measdivcst  26783  probfinmeasbOLD  26954  ptpcon  27265  cvmsval  27298  dfrtrclrec2  27488  rtrclreclem.refl  27489  climlec3  27544  prodmolem3  27589  prodmolem2a  27590  iprodmul  27646  bdayval  27932  imageval  28104  fvimage  28105  islocfin  28715  tailfval  28740  tailval  28741  heiborlem4  28860  heiborlem6  28862  mzpval  29215  mzpsubst  29232  rabdiophlem2  29287  fphpdo  29303  monotoddzz  29431  pw2f1o2val  29535  dnnumch3lem  29546  pwssplit4  29589  hbtlem1  29626  rgspnval  29672  refsum2cnlem1  29906  fmuldfeq  29911  stoweidlem26  29968  stoweidlem30  29972  stoweidlem31  29973  stoweidlem34  29976  stirlinglem5  30020  stirlinglem8  30023  wwlktovf1  30399  wwlktovfo  30400  wwlkn  30463  wlkiswwlksur  30498  wwlkextinj  30509  wwlkextsur  30510  clwwlkn  30577  clwwlkfv  30604  clwlkfoclwwlk  30665  clwlkf1clwwlk  30670  rusgranumwlklem1  30714  rusgranumwlklem3  30716  usg2spot2nb  30805  usgreg2spot  30807  2spotmdisj  30808  usgreghash2spot  30809  numclwlk1lem2fv  30833  numclwlk2lem2fv  30844  lincvalsc0  31073  linc0scn0  31075  linc1  31077  lincscm  31082  el0ldep  31118  bj-diagval  32848  lkrval  33056  pclvalN  33857  cdleme31fv  34357  docavalN  35091  dochval  35319  mapdval  35596  hvmapval  35728  hvmapvalvalN  35729  hdmap1vallem  35766  hdmapval  35799  hgmapval  35858