# Metamath Proof Explorer

## Theorem difprsnss

Description: Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion difprsnss ${⊢}\left\{{A},{B}\right\}\setminus \left\{{A}\right\}\subseteq \left\{{B}\right\}$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 1 elpr ${⊢}{x}\in \left\{{A},{B}\right\}↔\left({x}={A}\vee {x}={B}\right)$
3 velsn ${⊢}{x}\in \left\{{A}\right\}↔{x}={A}$
4 3 notbii ${⊢}¬{x}\in \left\{{A}\right\}↔¬{x}={A}$
5 biorf ${⊢}¬{x}={A}\to \left({x}={B}↔\left({x}={A}\vee {x}={B}\right)\right)$
6 5 biimparc ${⊢}\left(\left({x}={A}\vee {x}={B}\right)\wedge ¬{x}={A}\right)\to {x}={B}$
7 2 4 6 syl2anb ${⊢}\left({x}\in \left\{{A},{B}\right\}\wedge ¬{x}\in \left\{{A}\right\}\right)\to {x}={B}$
8 eldif ${⊢}{x}\in \left(\left\{{A},{B}\right\}\setminus \left\{{A}\right\}\right)↔\left({x}\in \left\{{A},{B}\right\}\wedge ¬{x}\in \left\{{A}\right\}\right)$
9 velsn ${⊢}{x}\in \left\{{B}\right\}↔{x}={B}$
10 7 8 9 3imtr4i ${⊢}{x}\in \left(\left\{{A},{B}\right\}\setminus \left\{{A}\right\}\right)\to {x}\in \left\{{B}\right\}$
11 10 ssriv ${⊢}\left\{{A},{B}\right\}\setminus \left\{{A}\right\}\subseteq \left\{{B}\right\}$