Description: A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016) (Proof shortened by Kyle Wyonch, 18-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | s1nz | ⊢ 〈“ 𝐴 ”〉 ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-s1 | ⊢ 〈“ 𝐴 ”〉 = { 〈 0 , ( I ‘ 𝐴 ) 〉 } | |
2 | opex | ⊢ 〈 0 , ( I ‘ 𝐴 ) 〉 ∈ V | |
3 | 2 | snnz | ⊢ { 〈 0 , ( I ‘ 𝐴 ) 〉 } ≠ ∅ |
4 | 1 3 | eqnetri | ⊢ 〈“ 𝐴 ”〉 ≠ ∅ |