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

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 ∈ V → A ∖ B ∈ 𝒫 A

Proof

Step Hyp Ref Expression
1 difss ⊢ A ∖ B ⊆ A
2 elpw2g ⊢ A ∈ V → A ∖ B ∈ 𝒫 A ↔ A ∖ B ⊆ A
3 1 2 mpbiri ⊢ A ∈ V → A ∖ B ∈ 𝒫 A