Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004)

	Ref	Expression
Assertion	disj	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\in A\neg x\in B$$

Proof

Step	Hyp	Ref	Expression
1		df-in	$$⊢A\cap B=\left\{x|\left(x\in A\wedge x\in B\right)\right\}$$
2	1	eqeq1i	$$⊢A\cap B=\varnothing \leftrightarrow \left\{x|\left(x\in A\wedge x\in B\right)\right\}=\varnothing$$
3		abeq1	$$⊢\left\{x|\left(x\in A\wedge x\in B\right)\right\}=\varnothing \leftrightarrow \forall x\left(\left(x\in A\wedge x\in B\right)\leftrightarrow x\in \varnothing \right)$$
4		imnan	$$⊢\left(x\in A\to \neg x\in B\right)\leftrightarrow \neg \left(x\in A\wedge x\in B\right)$$
5		noel	$$⊢\neg x\in \varnothing$$
6	5	nbn	$$⊢\neg \left(x\in A\wedge x\in B\right)\leftrightarrow \left(\left(x\in A\wedge x\in B\right)\leftrightarrow x\in \varnothing \right)$$
7	4 6	bitr2i	$$⊢\left(\left(x\in A\wedge x\in B\right)\leftrightarrow x\in \varnothing \right)\leftrightarrow \left(x\in A\to \neg x\in B\right)$$
8	7	albii	$$⊢\forall x\left(\left(x\in A\wedge x\in B\right)\leftrightarrow x\in \varnothing \right)\leftrightarrow \forall x\left(x\in A\to \neg x\in B\right)$$
9	2 3 8	3bitri	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\left(x\in A\to \neg x\in B\right)$$
10		df-ral	$$⊢\forall x\in A\neg x\in B\leftrightarrow \forall x\left(x\in A\to \neg x\in B\right)$$
11	9 10	bitr4i	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\in A\neg x\in B$$