Theorem difprsn2

Description: Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		prcom	$$⊢\left\{A,B\right\}=\left\{B,A\right\}$$
2	1	difeq1i	$$⊢\left\{A,B\right\}\setminus \left\{B\right\}=\left\{B,A\right\}\setminus \left\{B\right\}$$
3		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
4		difprsn1	$$⊢B\ne A\to \left\{B,A\right\}\setminus \left\{B\right\}=\left\{A\right\}$$
5	3 4	sylbi	$$⊢A\ne B\to \left\{B,A\right\}\setminus \left\{B\right\}=\left\{A\right\}$$
6	2 5	eqtrid	$$⊢A\ne B\to \left\{A,B\right\}\setminus \left\{B\right\}=\left\{A\right\}$$