# Metamath Proof Explorer

## 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 ${⊢}\left({A}\cap {B}=\varnothing \wedge {C}\in {A}\wedge {D}\in {B}\right)\to {C}\ne {D}$

### Proof

Step Hyp Ref Expression
1 disj ${⊢}{A}\cap {B}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}$
2 eleq1 ${⊢}{x}={C}\to \left({x}\in {B}↔{C}\in {B}\right)$
3 2 notbid ${⊢}{x}={C}\to \left(¬{x}\in {B}↔¬{C}\in {B}\right)$
4 3 rspccva ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\wedge {C}\in {A}\right)\to ¬{C}\in {B}$
5 eleq1a ${⊢}{D}\in {B}\to \left({C}={D}\to {C}\in {B}\right)$
6 5 necon3bd ${⊢}{D}\in {B}\to \left(¬{C}\in {B}\to {C}\ne {D}\right)$
7 4 6 syl5com ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}\wedge {C}\in {A}\right)\to \left({D}\in {B}\to {C}\ne {D}\right)$
8 1 7 sylanb ${⊢}\left({A}\cap {B}=\varnothing \wedge {C}\in {A}\right)\to \left({D}\in {B}\to {C}\ne {D}\right)$
9 8 3impia ${⊢}\left({A}\cap {B}=\varnothing \wedge {C}\in {A}\wedge {D}\in {B}\right)\to {C}\ne {D}$