Metamath Proof Explorer


Theorem funimass3

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion funimass3 Fun F A dom F F A B A F -1 B

Proof

Step Hyp Ref Expression
1 funimass4 Fun F A dom F F A B x A F x B
2 ssel A dom F x A x dom F
3 fvimacnv Fun F x dom F F x B x F -1 B
4 3 ex Fun F x dom F F x B x F -1 B
5 2 4 syl9r Fun F A dom F x A F x B x F -1 B
6 5 imp31 Fun F A dom F x A F x B x F -1 B
7 6 ralbidva Fun F A dom F x A F x B x A x F -1 B
8 1 7 bitrd Fun F A dom F F A B x A x F -1 B
9 dfss3 A F -1 B x A x F -1 B
10 8 9 bitr4di Fun F A dom F F A B A F -1 B