This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sspreima

Description: The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017)

Ref Expression
Assertion sspreima 
|- ( ( Fun F /\ A C_ B ) -> ( `' F " A ) C_ ( `' F " B ) )

Proof

Step Hyp Ref Expression
1 inpreima 
 |-  ( Fun F -> ( `' F " ( A i^i B ) ) = ( ( `' F " A ) i^i ( `' F " B ) ) )
2 dfss2 
 |-  ( A C_ B <-> ( A i^i B ) = A )
3 2 biimpi 
 |-  ( A C_ B -> ( A i^i B ) = A )
4 3 imaeq2d 
 |-  ( A C_ B -> ( `' F " ( A i^i B ) ) = ( `' F " A ) )
5 1 4 sylan9req 
 |-  ( ( Fun F /\ A C_ B ) -> ( ( `' F " A ) i^i ( `' F " B ) ) = ( `' F " A ) )
6 dfss2 
 |-  ( ( `' F " A ) C_ ( `' F " B ) <-> ( ( `' F " A ) i^i ( `' F " B ) ) = ( `' F " A ) )
7 5 6 sylibr 
 |-  ( ( Fun F /\ A C_ B ) -> ( `' F " A ) C_ ( `' F " B ) )