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

Metamath Proof Explorer

Theorem difpr

Description: Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018)

Ref Expression
Assertion difpr ⊢ A ∖ B C = A ∖ B ∖ C

Proof

Step Hyp Ref Expression
1 df-pr ⊢ B C = B ∪ C
2 1 difeq2i ⊢ A ∖ B C = A ∖ B ∪ C
3 difun1 ⊢ A ∖ B ∪ C = A ∖ B ∖ C
4 2 3 eqtri ⊢ A ∖ B C = A ∖ B ∖ C