Theorem fvmptg 5654

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 2204	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2216	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2211	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2947	. . . 4 |- E* y y = B
6	5	a1i 9	. . 3 |- ( x e. D -> E* y y = B )
7		fvmptg.2	. . . 4 |- F = ( x e. D |-> B )
8		df-mpt 4106	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2225	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5652	. 2 |- ( ( A e. D /\ C e. R ) -> ( C = C -> ( F ` A ) = C ) )
11	1, 10	mpi 15	1 |- ( ( A e. D /\ C e. R ) -> ( F ` A ) = C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1372   E*wmo 2054   e. wcel 2175   {copab 4103   |-> cmpt 4104   ` cfv 5270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-sbc 2998  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-iota 5231  df-fun 5272  df-fv 5278

This theorem is referenced by:  fvmpt  5655  fvmpts  5656  fvmpt3  5657  fvmpt2  5662  f1mpt  5839  caofinvl  6183  1stvalg  6227  2ndvalg  6228  brtpos2  6336  rdgon  6471  frec0g  6482  freccllem  6487  frecfcllem  6489  frecsuclem  6491  sucinc  6530  sucinc2  6531  omcl  6546  oeicl  6547  oav2  6548  omv2  6550  fvdiagfn  6779  djulclr  7150  djurclr  7151  djulcl  7152  djurcl  7153  djulclb  7156  omp1eomlem  7195  ctmlemr  7209  nnnninf  7227  nnnninfeq  7229  cardval3ex  7291  ceilqval  10449  frec2uzzd  10543  frec2uzsucd  10544  monoord2  10629  iseqf1olemqval  10643  iseqf1olemqk  10650  seq3f1olemqsum  10656  seq3f1oleml  10659  seq3f1o  10660  seq3distr  10675  ser3le  10680  hashinfom  10921  hashennn  10923  cjval  11127  reval  11131  imval  11132  cvg1nlemcau  11266  cvg1nlemres  11267  absval  11283  resqrexlemglsq  11304  resqrexlemga  11305  climmpt  11582  climle  11616  climcvg1nlem  11631  summodclem3  11662  summodclem2a  11663  zsumdc  11666  fsum3  11669  fsumcl2lem  11680  sumsnf  11691  isumadd  11713  fsumrev  11725  fsumshft  11726  fsummulc2  11730  iserabs  11757  isumlessdc  11778  divcnv  11779  trireciplem  11782  trirecip  11783  expcnvap0  11784  expcnvre  11785  expcnv  11786  explecnv  11787  geolim  11793  geolim2  11794  geo2lim  11798  geoisum  11799  geoisumr  11800  geoisum1  11801  geoisum1c  11802  cvgratz  11814  mertenslem2  11818  mertensabs  11819  fprodmul  11873  eftvalcn  11939  efval  11943  efcvgfsum  11949  ege2le3  11953  efcj  11955  eftlub  11972  efgt1p2  11977  eflegeo  11983  sinval  11984  cosval  11985  tanvalap  11990  eirraplem  12059  phival  12506  crth  12517  phimullem  12518  ennnfonelemj0  12743  ennnfonelem0  12747  strnfvnd  12823  topnvalg  13054  tgval  13065  2idlval  14235  zrhval  14350  toponsspwpwg  14465  cldval  14542  ntrfval  14543  clsfval  14544  neifval  14583  neival  14586  ismet  14787  isxmet  14788  divcnap  15008  mulc1cncf  15032  djucllem  15698  nnsf  15904  peano3nninf  15906  nninfself  15912  nninfsellemeqinf  15915  dceqnconst  15961  dcapnconst  15962