Theorem difprsn1

Description: Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017)

	Ref	Expression
Assertion	difprsn1	$$⊢A\ne B\to \left\{A,B\right\}\setminus \left\{A\right\}=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		necom	$$⊢B\ne A\leftrightarrow A\ne B$$
2		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
3	2	equncomi	$$⊢\left\{A,B\right\}=\left\{B\right\}\cup \left\{A\right\}$$
4	3	difeq1i	$$⊢\left\{A,B\right\}\setminus \left\{A\right\}=\left(\left\{B\right\}\cup \left\{A\right\}\right)\setminus \left\{A\right\}$$
5		difun2	$$⊢\left(\left\{B\right\}\cup \left\{A\right\}\right)\setminus \left\{A\right\}=\left\{B\right\}\setminus \left\{A\right\}$$
6	4 5	eqtri	$$⊢\left\{A,B\right\}\setminus \left\{A\right\}=\left\{B\right\}\setminus \left\{A\right\}$$
7		disjsn2	$$⊢B\ne A\to \left\{B\right\}\cap \left\{A\right\}=\varnothing$$
8		disj3	$$⊢\left\{B\right\}\cap \left\{A\right\}=\varnothing \leftrightarrow \left\{B\right\}=\left\{B\right\}\setminus \left\{A\right\}$$
9	7 8	sylib	$$⊢B\ne A\to \left\{B\right\}=\left\{B\right\}\setminus \left\{A\right\}$$
10	6 9	eqtr4id	$$⊢B\ne A\to \left\{A,B\right\}\setminus \left\{A\right\}=\left\{B\right\}$$
11	1 10	sylbir	$$⊢A\ne B\to \left\{A,B\right\}\setminus \left\{A\right\}=\left\{B\right\}$$