Metamath Proof Explorer


Theorem bnj1503

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1503.1
|- ( ph -> Fun F )
bnj1503.2
|- ( ph -> G C_ F )
bnj1503.3
|- ( ph -> A C_ dom G )
Assertion bnj1503
|- ( ph -> ( F |` A ) = ( G |` A ) )

Proof

Step Hyp Ref Expression
1 bnj1503.1
 |-  ( ph -> Fun F )
2 bnj1503.2
 |-  ( ph -> G C_ F )
3 bnj1503.3
 |-  ( ph -> A C_ dom G )
4 fun2ssres
 |-  ( ( Fun F /\ G C_ F /\ A C_ dom G ) -> ( F |` A ) = ( G |` A ) )
5 1 2 3 4 syl3anc
 |-  ( ph -> ( F |` A ) = ( G |` A ) )