Theorem fvmptg 5655

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 2205	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2217	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2212	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2948	. . . 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 4107	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2226	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5653	. 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 1373   E*wmo 2055   e. wcel 2176   {copab 4104   |-> cmpt 4105   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-mpt 4107  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-iota 5232  df-fun 5273  df-fv 5279

This theorem is referenced by:  fvmpt  5656  fvmpts  5657  fvmpt3  5658  fvmpt2  5663  f1mpt  5840  caofinvl  6184  1stvalg  6228  2ndvalg  6229  brtpos2  6337  rdgon  6472  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  sucinc  6531  sucinc2  6532  omcl  6547  oeicl  6548  oav2  6549  omv2  6551  fvdiagfn  6780  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djulclb  7157  omp1eomlem  7196  ctmlemr  7210  nnnninf  7228  nnnninfeq  7230  cardval3ex  7292  ceilqval  10451  frec2uzzd  10545  frec2uzsucd  10546  monoord2  10631  iseqf1olemqval  10645  iseqf1olemqk  10652  seq3f1olemqsum  10658  seq3f1oleml  10661  seq3f1o  10662  seq3distr  10677  ser3le  10682  hashinfom  10923  hashennn  10925  cjval  11156  reval  11160  imval  11161  cvg1nlemcau  11295  cvg1nlemres  11296  absval  11312  resqrexlemglsq  11333  resqrexlemga  11334  climmpt  11611  climle  11645  climcvg1nlem  11660  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsum3  11698  fsumcl2lem  11709  sumsnf  11720  isumadd  11742  fsumrev  11754  fsumshft  11755  fsummulc2  11759  iserabs  11786  isumlessdc  11807  divcnv  11808  trireciplem  11811  trirecip  11812  expcnvap0  11813  expcnvre  11814  expcnv  11815  explecnv  11816  geolim  11822  geolim2  11823  geo2lim  11827  geoisum  11828  geoisumr  11829  geoisum1  11830  geoisum1c  11831  cvgratz  11843  mertenslem2  11847  mertensabs  11848  fprodmul  11902  eftvalcn  11968  efval  11972  efcvgfsum  11978  ege2le3  11982  efcj  11984  eftlub  12001  efgt1p2  12006  eflegeo  12012  sinval  12013  cosval  12014  tanvalap  12019  eirraplem  12088  phival  12535  crth  12546  phimullem  12547  ennnfonelemj0  12772  ennnfonelem0  12776  strnfvnd  12852  topnvalg  13083  tgval  13094  2idlval  14264  zrhval  14379  toponsspwpwg  14494  cldval  14571  ntrfval  14572  clsfval  14573  neifval  14612  neival  14615  ismet  14816  isxmet  14817  divcnap  15037  mulc1cncf  15061  djucllem  15736  nnsf  15942  peano3nninf  15944  nninfself  15950  nninfsellemeqinf  15953  dceqnconst  15999  dcapnconst  16000