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\setminus \left\{B,C\right\}=\left(A\setminus \left\{B\right\}\right)\setminus \left\{C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{B,C\right\}=\left\{B\right\}\cup \left\{C\right\}$$
2	1	difeq2i	$$⊢A\setminus \left\{B,C\right\}=A\setminus \left(\left\{B\right\}\cup \left\{C\right\}\right)$$
3		difun1	$$⊢A\setminus \left(\left\{B\right\}\cup \left\{C\right\}\right)=\left(A\setminus \left\{B\right\}\right)\setminus \left\{C\right\}$$
4	2 3	eqtri	$$⊢A\setminus \left\{B,C\right\}=\left(A\setminus \left\{B\right\}\right)\setminus \left\{C\right\}$$