# Metamath Proof Explorer

## 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}↔{A}\ne {B}$
2 disjsn2 ${⊢}{B}\ne {A}\to \left\{{B}\right\}\cap \left\{{A}\right\}=\varnothing$
3 disj3 ${⊢}\left\{{B}\right\}\cap \left\{{A}\right\}=\varnothing ↔\left\{{B}\right\}=\left\{{B}\right\}\setminus \left\{{A}\right\}$
4 2 3 sylib ${⊢}{B}\ne {A}\to \left\{{B}\right\}=\left\{{B}\right\}\setminus \left\{{A}\right\}$
5 df-pr ${⊢}\left\{{A},{B}\right\}=\left\{{A}\right\}\cup \left\{{B}\right\}$
6 5 equncomi ${⊢}\left\{{A},{B}\right\}=\left\{{B}\right\}\cup \left\{{A}\right\}$
7 6 difeq1i ${⊢}\left\{{A},{B}\right\}\setminus \left\{{A}\right\}=\left(\left\{{B}\right\}\cup \left\{{A}\right\}\right)\setminus \left\{{A}\right\}$
8 difun2 ${⊢}\left(\left\{{B}\right\}\cup \left\{{A}\right\}\right)\setminus \left\{{A}\right\}=\left\{{B}\right\}\setminus \left\{{A}\right\}$
9 7 8 eqtri ${⊢}\left\{{A},{B}\right\}\setminus \left\{{A}\right\}=\left\{{B}\right\}\setminus \left\{{A}\right\}$
10 4 9 syl6reqr ${⊢}{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\}$