Metamath Proof Explorer


Theorem difpreima

Description: Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016)

Ref Expression
Assertion difpreima Fun F F -1 A B = F -1 A F -1 B

Proof

Step Hyp Ref Expression
1 funcnvcnv Fun F Fun F -1 -1
2 imadif Fun F -1 -1 F -1 A B = F -1 A F -1 B
3 1 2 syl Fun F F -1 A B = F -1 A F -1 B