Theorem disjsn

Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

	Ref	Expression
Assertion	disjsn	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		disj1	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 } ) )
2		con2b	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 } ) ↔ ( 𝑥 ∈ { 𝐵 } → ¬ 𝑥 ∈ 𝐴 ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
4	3	imbi1i	⊢ ( ( 𝑥 ∈ { 𝐵 } → ¬ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴 ) )
5		imnan	⊢ ( ( 𝑥 = 𝐵 → ¬ 𝑥 ∈ 𝐴 ) ↔ ¬ ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
6	2 4 5	3bitri	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 } ) ↔ ¬ ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
7	6	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ { 𝐵 } ) ↔ ∀ 𝑥 ¬ ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
8		alnex	⊢ ( ∀ 𝑥 ¬ ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
9		dfclel	⊢ ( 𝐵 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
10	8 9	xchbinxr	⊢ ( ∀ 𝑥 ¬ ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) ↔ ¬ 𝐵 ∈ 𝐴 )
11	1 7 10	3bitri	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )