Metamath Proof Explorer


Theorem sndisj

Description: Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion sndisj Disj 𝑥𝐴 { 𝑥 }

Proof

Step Hyp Ref Expression
1 dfdisj2 ( Disj 𝑥𝐴 { 𝑥 } ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥𝐴𝑦 ∈ { 𝑥 } ) )
2 moeq ∃* 𝑥 𝑥 = 𝑦
3 simpr ( ( 𝑥𝐴𝑦 ∈ { 𝑥 } ) → 𝑦 ∈ { 𝑥 } )
4 velsn ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
5 3 4 sylib ( ( 𝑥𝐴𝑦 ∈ { 𝑥 } ) → 𝑦 = 𝑥 )
6 5 equcomd ( ( 𝑥𝐴𝑦 ∈ { 𝑥 } ) → 𝑥 = 𝑦 )
7 6 moimi ( ∃* 𝑥 𝑥 = 𝑦 → ∃* 𝑥 ( 𝑥𝐴𝑦 ∈ { 𝑥 } ) )
8 2 7 ax-mp ∃* 𝑥 ( 𝑥𝐴𝑦 ∈ { 𝑥 } )
9 1 8 mpgbir Disj 𝑥𝐴 { 𝑥 }