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		df-ss	|- ( 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		df-ss	|- ( ( `' 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 ) )