Theorem frmdelbas

Description: An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
	frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
Assertion	frmdelbas	$$⊢X\in B\to X\in \mathrm{Word}I$$

Proof

Step	Hyp	Ref	Expression
1		frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
2		frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
3		id	$$⊢X\in B\to X\in B$$
4	1 2	elbasfv	$$⊢X\in B\to I\in \mathrm{V}$$
5	1 2	frmdbas	$$⊢I\in \mathrm{V}\to B=\mathrm{Word}I$$
6	4 5	syl	$$⊢X\in B\to B=\mathrm{Word}I$$
7	3 6	eleqtrd	$$⊢X\in B\to X\in \mathrm{Word}I$$