Metamath Proof Explorer

Theorem difpreima

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

Ref Expression
Assertion difpreima 
|- ( Fun F -> ( `' F " ( A \ B ) ) = ( ( `' F " A ) \ ( `' F " B ) ) )

Proof

Step Hyp Ref Expression
1 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
2 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( A \ B ) ) = ( ( `' F " A ) \ ( `' F " B ) ) )
3 1 2 syl 
 |-  ( Fun F -> ( `' F " ( A \ B ) ) = ( ( `' F " A ) \ ( `' F " B ) ) )