Theorem fvmptg 5637

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 2196	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2208	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2203	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2939	. . . 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 4096	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2217	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5635	. 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 1364   E*wmo 2046   e. wcel 2167   {copab 4093   |-> cmpt 4094   ` cfv 5258

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-mpt 4096  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-iota 5219  df-fun 5260  df-fv 5266

This theorem is referenced by:  fvmpt  5638  fvmpts  5639  fvmpt3  5640  fvmpt2  5645  f1mpt  5818  caofinvl  6160  1stvalg  6200  2ndvalg  6201  brtpos2  6309  rdgon  6444  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  sucinc  6503  sucinc2  6504  omcl  6519  oeicl  6520  oav2  6521  omv2  6523  fvdiagfn  6752  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  djulclb  7121  omp1eomlem  7160  ctmlemr  7174  nnnninf  7192  nnnninfeq  7194  cardval3ex  7252  ceilqval  10398  frec2uzzd  10492  frec2uzsucd  10493  monoord2  10578  iseqf1olemqval  10592  iseqf1olemqk  10599  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  seq3distr  10624  ser3le  10629  hashinfom  10870  hashennn  10872  cjval  11010  reval  11014  imval  11015  cvg1nlemcau  11149  cvg1nlemres  11150  absval  11166  resqrexlemglsq  11187  resqrexlemga  11188  climmpt  11465  climle  11499  climcvg1nlem  11514  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsum3  11552  fsumcl2lem  11563  sumsnf  11574  isumadd  11596  fsumrev  11608  fsumshft  11609  fsummulc2  11613  iserabs  11640  isumlessdc  11661  divcnv  11662  trireciplem  11665  trirecip  11666  expcnvap0  11667  expcnvre  11668  expcnv  11669  explecnv  11670  geolim  11676  geolim2  11677  geo2lim  11681  geoisum  11682  geoisumr  11683  geoisum1  11684  geoisum1c  11685  cvgratz  11697  mertenslem2  11701  mertensabs  11702  fprodmul  11756  eftvalcn  11822  efval  11826  efcvgfsum  11832  ege2le3  11836  efcj  11838  eftlub  11855  efgt1p2  11860  eflegeo  11866  sinval  11867  cosval  11868  tanvalap  11873  eirraplem  11942  phival  12381  crth  12392  phimullem  12393  ennnfonelemj0  12618  ennnfonelem0  12622  strnfvnd  12698  topnvalg  12922  tgval  12933  2idlval  14058  zrhval  14173  toponsspwpwg  14258  cldval  14335  ntrfval  14336  clsfval  14337  neifval  14376  neival  14379  ismet  14580  isxmet  14581  divcnap  14801  mulc1cncf  14825  djucllem  15446  nnsf  15649  peano3nninf  15651  nninfself  15657  nninfsellemeqinf  15660  dceqnconst  15704  dcapnconst  15705