Theorem fvmptg 5722

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 2231	. 2 |- C = C
2		fvmptg.1	. . . 4 |- ( x = A -> B = C )
3	2	eqeq2d 2243	. . 3 |- ( x = A -> ( y = B <-> y = C ) )
4		eqeq1 2238	. . 3 |- ( y = C -> ( y = C <-> C = C ) )
5		moeq 2981	. . . 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 4152	. . . 4 |- ( x e. D |-> B ) = { <. x , y >. | ( x e. D /\ y = B ) }
9	7, 8	eqtri 2252	. . 3 |- F = { <. x , y >. | ( x e. D /\ y = B ) }
10	3, 4, 6, 9	fvopab3ig 5720	. 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 1397   E*wmo 2080   e. wcel 2202   {copab 4149   |-> cmpt 4150   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334

This theorem is referenced by:  fvmpt  5723  fvmpts  5724  fvmpt3  5725  fvmpt2  5730  f1mpt  5912  caofinvl  6261  1stvalg  6305  2ndvalg  6306  brtpos2  6417  rdgon  6552  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  sucinc  6613  sucinc2  6614  omcl  6629  oeicl  6630  oav2  6631  omv2  6633  fvdiagfn  6862  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djulclb  7254  omp1eomlem  7293  ctmlemr  7307  nnnninf  7325  nnnninfeq  7327  cardval3ex  7389  ceilqval  10569  frec2uzzd  10663  frec2uzsucd  10664  monoord2  10749  iseqf1olemqval  10763  iseqf1olemqk  10770  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seq3distr  10795  ser3le  10800  hashinfom  11041  hashennn  11043  cjval  11423  reval  11427  imval  11428  cvg1nlemcau  11562  cvg1nlemres  11563  absval  11579  resqrexlemglsq  11600  resqrexlemga  11601  climmpt  11878  climle  11912  climcvg1nlem  11927  summodclem3  11959  summodclem2a  11960  zsumdc  11963  fsum3  11966  fsumcl2lem  11977  sumsnf  11988  isumadd  12010  fsumrev  12022  fsumshft  12023  fsummulc2  12027  iserabs  12054  isumlessdc  12075  divcnv  12076  trireciplem  12079  trirecip  12080  expcnvap0  12081  expcnvre  12082  expcnv  12083  explecnv  12084  geolim  12090  geolim2  12091  geo2lim  12095  geoisum  12096  geoisumr  12097  geoisum1  12098  geoisum1c  12099  cvgratz  12111  mertenslem2  12115  mertensabs  12116  fprodmul  12170  eftvalcn  12236  efval  12240  efcvgfsum  12246  ege2le3  12250  efcj  12252  eftlub  12269  efgt1p2  12274  eflegeo  12280  sinval  12281  cosval  12282  tanvalap  12287  eirraplem  12356  phival  12803  crth  12814  phimullem  12815  ennnfonelemj0  13040  ennnfonelem0  13044  strnfvnd  13120  topnvalg  13352  tgval  13363  2idlval  14535  zrhval  14650  toponsspwpwg  14765  cldval  14842  ntrfval  14843  clsfval  14844  neifval  14883  neival  14886  ismet  15087  isxmet  15088  divcnap  15308  mulc1cncf  15332  depindlem1  16376  djucllem  16447  nnsf  16658  peano3nninf  16660  nninfself  16666  nninfsellemeqinf  16669  dceqnconst  16716  dcapnconst  16717