# Metamath Proof Explorer

## Theorem disjsn

Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

Ref Expression
Assertion disjsn ${⊢}{A}\cap \left\{{B}\right\}=\varnothing ↔¬{B}\in {A}$

### Proof

Step Hyp Ref Expression
1 disj1 ${⊢}{A}\cap \left\{{B}\right\}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in \left\{{B}\right\}\right)$
2 con2b ${⊢}\left({x}\in {A}\to ¬{x}\in \left\{{B}\right\}\right)↔\left({x}\in \left\{{B}\right\}\to ¬{x}\in {A}\right)$
3 velsn ${⊢}{x}\in \left\{{B}\right\}↔{x}={B}$
4 3 imbi1i ${⊢}\left({x}\in \left\{{B}\right\}\to ¬{x}\in {A}\right)↔\left({x}={B}\to ¬{x}\in {A}\right)$
5 imnan ${⊢}\left({x}={B}\to ¬{x}\in {A}\right)↔¬\left({x}={B}\wedge {x}\in {A}\right)$
6 2 4 5 3bitri ${⊢}\left({x}\in {A}\to ¬{x}\in \left\{{B}\right\}\right)↔¬\left({x}={B}\wedge {x}\in {A}\right)$
7 6 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in \left\{{B}\right\}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}={B}\wedge {x}\in {A}\right)$
8 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}={B}\wedge {x}\in {A}\right)↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge {x}\in {A}\right)$
9 dfclel ${⊢}{B}\in {A}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge {x}\in {A}\right)$
10 8 9 xchbinxr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}={B}\wedge {x}\in {A}\right)↔¬{B}\in {A}$
11 1 7 10 3bitri ${⊢}{A}\cap \left\{{B}\right\}=\varnothing ↔¬{B}\in {A}$