repsw0

Description: The "repeated symbol word" of length 0. (Contributed by AV, 4-Nov-2018)

		Ref	Expression
	Assertion	repsw0	$⊢ S \in V \to S repeatS 0 = \emptyset$

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		repswlen	$⊢ (S \in V \land 0 \in ℕ_{0}) \to \|S repeatS 0\| = 0$
3	1 2	mpan2	$⊢ S \in V \to \|S repeatS 0\| = 0$
4		ovex	$⊢ S repeatS 0 \in V$
5		hasheq0	$⊢ S repeatS 0 \in V \to (\|S repeatS 0\| = 0 \leftrightarrow S repeatS 0 = \emptyset)$
6	4 5	mp1i	$⊢ S \in V \to (\|S repeatS 0\| = 0 \leftrightarrow S repeatS 0 = \emptyset)$
7	3 6	mpbid	$⊢ S \in V \to S repeatS 0 = \emptyset$

Metamath Proof Explorer