Theorem fvmptg 5784

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 2238	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2250	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2245	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 3001	. . . 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 4195	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2259	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5782	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   E*wmo 2087   e. wcel 2209   {copab 4192   |-> cmpt 4193   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388

This theorem is used by:  fvmpt  5785  fvmpts  5786  fvmpt3  5787  fvmpt2  5792  f1mpt  5980  caofinvl  6332  1stvalg  6380  2ndvalg  6381  brtpos2  6526  rdgon  6661  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  sucinc  6722  sucinc2  6723  omcl  6738  oeicl  6739  oav2  6740  omv2  6742  fvdiagfn  6979  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djulclb  7401  omp1eomlem  7440  ctmlemr  7454  nnnninf  7472  nnnninfeq  7474  cardval3ex  7536  ceilqval  10764  frec2uzzd  10858  frec2uzsucd  10859  monoord2  10944  iseqf1olemqval  10958  iseqf1olemqk  10965  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  seq3distr  10990  ser3le  10995  hashinfom  11239  hashennn  11241  cjval  11632  reval  11636  imval  11637  cvg1nlemcau  11772  cvg1nlemres  11773  absval  11789  resqrexlemglsq  11810  resqrexlemga  11811  climmpt  12091  climle  12125  climcvg1nlem  12140  summodclem3  12172  summodclem2a  12173  zsumdc  12176  fsum3  12179  fsumcl2lem  12190  sumsnf  12201  isumadd  12223  fsumrev  12235  fsumshft  12236  fsummulc2  12240  iserabs  12267  isumlessdc  12288  divcnv  12289  trireciplem  12292  trirecip  12293  expcnvap0  12294  expcnvre  12295  expcnv  12296  explecnv  12297  geolim  12303  geolim2  12304  geo2lim  12308  geoisum  12309  geoisumr  12310  geoisum1  12311  geoisum1c  12312  cvgratz  12324  mertenslem2  12328  mertensabs  12329  fprodmul  12383  eftvalcn  12449  efval  12453  efcvgfsum  12459  ege2le3  12463  efcj  12465  eftlub  12482  efgt1p2  12487  eflegeo  12493  sinval  12494  cosval  12495  tanvalap  12500  eirraplem  12569  phival  13020  crth  13031  phimullem  13032  ennnfonelemj0  13350  ennnfonelem0  13354  strnfvnd  13430  topnvalg  13664  tgval  13675  2idlval  14948  zrhval  15061  toponsspwpwg  15248  cldval  15325  ntrfval  15326  clsfval  15327  neifval  15366  neival  15369  ismet  15570  isxmet  15571  divcnap  15791  mulc1cncf  15815  depindlem1  16952  djucllem  17033  nnsf  17254  peano3nninf  17256  nninfself  17262  nninfsellemeqinf  17265  dceqnconst  17317  dcapnconst  17318