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	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		disj	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
3	1 2	bitri	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )