**Description:** A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015)

Ref | Expression | ||
---|---|---|---|

Assertion | disjel | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 ∈ 𝐵 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | disj3 | ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ 𝐵 ) ) | |

2 | eleq2 | ⊢ ( 𝐴 = ( 𝐴 ∖ 𝐵 ) → ( 𝐶 ∈ 𝐴 ↔ 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) ) ) | |

3 | eldifn | ⊢ ( 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ 𝐶 ∈ 𝐵 ) | |

4 | 2 3 | syl6bi | ⊢ ( 𝐴 = ( 𝐴 ∖ 𝐵 ) → ( 𝐶 ∈ 𝐴 → ¬ 𝐶 ∈ 𝐵 ) ) |

5 | 1 4 | sylbi | ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∈ 𝐴 → ¬ 𝐶 ∈ 𝐵 ) ) |

6 | 5 | imp | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 ∈ 𝐵 ) |