Theorem disjne

Description: Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	disjne	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → 𝐶 ≠ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		disj	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
2		eleq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵 ) )
3	2	notbid	⊢ ( 𝑥 = 𝐶 → ( ¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝐶 ∈ 𝐵 ) )
4	3	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 ∈ 𝐵 )
5		eleq1a	⊢ ( 𝐷 ∈ 𝐵 → ( 𝐶 = 𝐷 → 𝐶 ∈ 𝐵 ) )
6	5	necon3bd	⊢ ( 𝐷 ∈ 𝐵 → ( ¬ 𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐷 ) )
7	4 6	syl5com	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ∈ 𝐵 → 𝐶 ≠ 𝐷 ) )
8	1 7	sylanb	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ∈ 𝐵 → 𝐶 ≠ 𝐷 ) )
9	8	3impia	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → 𝐶 ≠ 𝐷 )