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	⊢ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) = ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐵 , 𝐶 } = ( { 𝐵 } ∪ { 𝐶 } )
2	1	difeq2i	⊢ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) = ( 𝐴 ∖ ( { 𝐵 } ∪ { 𝐶 } ) )
3		difun1	⊢ ( 𝐴 ∖ ( { 𝐵 } ∪ { 𝐶 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } )
4	2 3	eqtri	⊢ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) = ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } )