Metamath Proof Explorer


Theorem funimass2

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004)

Ref Expression
Assertion funimass2 Fun F A F -1 B F A B

Proof

Step Hyp Ref Expression
1 funimacnv Fun F F F -1 B = B ran F
2 1 sseq2d Fun F F A F F -1 B F A B ran F
3 inss1 B ran F B
4 sstr2 F A B ran F B ran F B F A B
5 3 4 mpi F A B ran F F A B
6 2 5 syl6bi Fun F F A F F -1 B F A B
7 imass2 A F -1 B F A F F -1 B
8 6 7 impel Fun F A F -1 B F A B