Theorem fvmptg 5753

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 2232	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2244	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2239	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2992	. . . 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 4173	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2253	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5751	. 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 1398   E*wmo 2081   e. wcel 2203   {copab 4170   |-> cmpt 4171   ` cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360

This theorem is referenced by:  fvmpt  5754  fvmpts  5755  fvmpt3  5756  fvmpt2  5761  f1mpt  5944  caofinvl  6292  1stvalg  6336  2ndvalg  6337  brtpos2  6482  rdgon  6617  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  sucinc  6678  sucinc2  6679  omcl  6694  oeicl  6695  oav2  6696  omv2  6698  fvdiagfn  6928  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djulclb  7346  omp1eomlem  7385  ctmlemr  7399  nnnninf  7417  nnnninfeq  7419  cardval3ex  7481  ceilqval  10668  frec2uzzd  10762  frec2uzsucd  10763  monoord2  10848  iseqf1olemqval  10862  iseqf1olemqk  10869  seq3f1olemqsum  10875  seq3f1oleml  10878  seq3f1o  10879  seq3distr  10894  ser3le  10899  hashinfom  11141  hashennn  11143  cjval  11530  reval  11534  imval  11535  cvg1nlemcau  11669  cvg1nlemres  11670  absval  11686  resqrexlemglsq  11707  resqrexlemga  11708  climmpt  11985  climle  12019  climcvg1nlem  12034  summodclem3  12066  summodclem2a  12067  zsumdc  12070  fsum3  12073  fsumcl2lem  12084  sumsnf  12095  isumadd  12117  fsumrev  12129  fsumshft  12130  fsummulc2  12134  iserabs  12161  isumlessdc  12182  divcnv  12183  trireciplem  12186  trirecip  12187  expcnvap0  12188  expcnvre  12189  expcnv  12190  explecnv  12191  geolim  12197  geolim2  12198  geo2lim  12202  geoisum  12203  geoisumr  12204  geoisum1  12205  geoisum1c  12206  cvgratz  12218  mertenslem2  12222  mertensabs  12223  fprodmul  12277  eftvalcn  12343  efval  12347  efcvgfsum  12353  ege2le3  12357  efcj  12359  eftlub  12376  efgt1p2  12381  eflegeo  12387  sinval  12388  cosval  12389  tanvalap  12394  eirraplem  12463  phival  12910  crth  12921  phimullem  12922  ennnfonelemj0  13152  ennnfonelem0  13156  strnfvnd  13232  topnvalg  13464  tgval  13475  2idlval  14650  zrhval  14765  toponsspwpwg  14887  cldval  14964  ntrfval  14965  clsfval  14966  neifval  15005  neival  15008  ismet  15209  isxmet  15210  divcnap  15430  mulc1cncf  15454  depindlem1  16501  djucllem  16572  nnsf  16783  peano3nninf  16785  nninfself  16791  nninfsellemeqinf  16794  dceqnconst  16846  dcapnconst  16847