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 FunFABF-1AF-1B

Proof

Step Hyp Ref Expression
1 inpreima FunFF-1AB=F-1AF-1B
2 df-ss ABAB=A
3 2 biimpi ABAB=A
4 3 imaeq2d ABF-1AB=F-1A
5 1 4 sylan9req FunFABF-1AF-1B=F-1A
6 df-ss F-1AF-1BF-1AF-1B=F-1A
7 5 6 sylibr FunFABF-1AF-1B