# Metamath Proof Explorer

## Theorem disj3

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998)

Ref Expression
Assertion disj3 ${⊢}{A}\cap {B}=\varnothing ↔{A}={A}\setminus {B}$

### Proof

Step Hyp Ref Expression
1 pm4.71 ${⊢}\left({x}\in {A}\to ¬{x}\in {B}\right)↔\left({x}\in {A}↔\left({x}\in {A}\wedge ¬{x}\in {B}\right)\right)$
2 eldif ${⊢}{x}\in \left({A}\setminus {B}\right)↔\left({x}\in {A}\wedge ¬{x}\in {B}\right)$
3 2 bibi2i ${⊢}\left({x}\in {A}↔{x}\in \left({A}\setminus {B}\right)\right)↔\left({x}\in {A}↔\left({x}\in {A}\wedge ¬{x}\in {B}\right)\right)$
4 1 3 bitr4i ${⊢}\left({x}\in {A}\to ¬{x}\in {B}\right)↔\left({x}\in {A}↔{x}\in \left({A}\setminus {B}\right)\right)$
5 4 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in \left({A}\setminus {B}\right)\right)$
6 disj1 ${⊢}{A}\cap {B}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {B}\right)$
7 dfcleq ${⊢}{A}={A}\setminus {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in \left({A}\setminus {B}\right)\right)$
8 5 6 7 3bitr4i ${⊢}{A}\cap {B}=\varnothing ↔{A}={A}\setminus {B}$