This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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