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

Metamath Proof Explorer

Theorem s1nz

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	$⊢ ⟨“ A ”⟩ \neq \emptyset$

Step	Hyp	Ref	Expression
1		df-s1	$⊢ ⟨“ A ”⟩ = \{⟨0, I (A)⟩\}$
2		opex	$⊢ ⟨0, I (A)⟩ \in V$
3	2	snnz	$⊢ \{⟨0, I (A)⟩\} \neq \emptyset$
4	1 3	eqnetri	$⊢ ⟨“ A ”⟩ \neq \emptyset$