Metamath Proof Explorer

Theorem difelpw

Description: A difference is an element of the power set of its minuend. (Contributed by AV, 9-Oct-2023)

Ref Expression
Assertion difelpw 
|- ( A e. V -> ( A \ B ) e. ~P A )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( A \ B ) C_ A
2 elpw2g 
 |-  ( A e. V -> ( ( A \ B ) e. ~P A <-> ( A \ B ) C_ A ) )
3 1 2 mpbiri 
 |-  ( A e. V -> ( A \ B ) e. ~P A )