Theorem disjel

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

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

Proof

Step	Hyp	Ref	Expression
1		disj3	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ 𝐵 ) )
2		eleq2	⊢ ( 𝐴 = ( 𝐴 ∖ 𝐵 ) → ( 𝐶 ∈ 𝐴 ↔ 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) ) )
3		eldifn	⊢ ( 𝐶 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ 𝐶 ∈ 𝐵 )
4	2 3	biimtrdi	⊢ ( 𝐴 = ( 𝐴 ∖ 𝐵 ) → ( 𝐶 ∈ 𝐴 → ¬ 𝐶 ∈ 𝐵 ) )
5	1 4	sylbi	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∈ 𝐴 → ¬ 𝐶 ∈ 𝐵 ) )
6	5	imp	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 ∈ 𝐵 )