Theorem funssfv 5804

Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994.)

Assertion

Ref	Expression
funssfv	|- ( ( Fun F /\ G C_ F /\ A e. dom G ) -> ( F ` A ) = ( G ` A ) )

Proof of Theorem funssfv

Step	Hyp	Ref	Expression
1		fvres 5803	. . . 4 |- ( A e. dom G -> ( ( F |` dom G ) ` A ) = ( F ` A ) )
2	1	eqcomd 2459	. . 3 |- ( A e. dom G -> ( F ` A ) = ( ( F |` dom G ) ` A ) )
3		funssres 5556	. . . 4 |- ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )
4	3	fveq1d 5791	. . 3 |- ( ( Fun F /\ G C_ F ) -> ( ( F |` dom G ) ` A ) = ( G ` A ) )
5	2, 4	sylan9eqr 2514	. 2 |- ( ( ( Fun F /\ G C_ F ) /\ A e. dom G ) -> ( F ` A ) = ( G ` A ) )
6	5	3impa 1183	1 |- ( ( Fun F /\ G C_ F /\ A e. dom G ) -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   C_ wss 3426   dom cdm 4938   |` cres 4940   Fun wfun 5510   ` cfv 5516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-res 4950  df-iota 5479  df-fun 5518  df-fv 5524

This theorem is referenced by:  funsssuppss  6815  tfrlem9  6944  tfrlem11  6947  ac6sfi  7657  axdc3lem2  8721  axdc3lem4  8723  imasvscaval  14578  pserdv  22010  eupap1  23732  sspn  24269  subfacp1lem2a  27202  subfacp1lem2b  27203  subfacp1lem5  27206  cvmliftlem10  27317  cvmliftlem13  27319  wfrlem12  27869  wfrlem14  27871  frrlem11  27914  bnj945  32067  bnj1502  32141  bnj545  32188  bnj548  32190