This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )