Theorem funssfv 5820

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 5819	. . . 4 |- ( A e. dom G -> ( ( F |` dom G ) ` A ) = ( F ` A ) )
2	1	eqcomd 2410	. . 3 |- ( A e. dom G -> ( F ` A ) = ( ( F |` dom G ) ` A ) )
3		funssres 5565	. . . 4 |- ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )
4	3	fveq1d 5807	. . 3 |- ( ( Fun F /\ G C_ F ) -> ( ( F |` dom G ) ` A ) = ( G ` A ) )
5	2, 4	sylan9eqr 2465	. 2 |- ( ( ( Fun F /\ G C_ F ) /\ A e. dom G ) -> ( F ` A ) = ( G ` A ) )
6	5	3impa 1192	1 |- ( ( Fun F /\ G C_ F /\ A e. dom G ) -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   C_ wss 3413   dom cdm 4942   |` cres 4944   Fun wfun 5519   ` cfv 5525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-id 4737  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-res 4954  df-iota 5489  df-fun 5527  df-fv 5533

This theorem is referenced by:  funsssuppss  6883  tfrlem9  7011  tfrlem11  7014  ac6sfi  7718  axdc3lem2  8783  axdc3lem4  8785  imasvscaval  15044  pserdv  23008  eupap1  25274  sspn  25943  bnj945  29040  bnj1502  29114  bnj545  29161  bnj548  29163  subfacp1lem2a  29358  subfacp1lem2b  29359  subfacp1lem5  29362  cvmliftlem10  29472  cvmliftlem13  29474  wfrlem12  30027  wfrlem14  30029  frrlem11  30072