Theorem disj1

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

	Ref	Expression
Assertion	disj1	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\left(x\in A\to \neg x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		disj	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\in A\neg x\in B$$
2		df-ral	$$⊢\forall x\in A\neg x\in B\leftrightarrow \forall x\left(x\in A\to \neg x\in B\right)$$
3	1 2	bitri	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\left(x\in A\to \neg x\in B\right)$$