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 = ( freeMnd ` I )
	frmdbas.b	|- B = ( Base ` M )
Assertion	frmdelbas	|- ( X e. B -> X e. Word I )

Proof

Step	Hyp	Ref	Expression
1		frmdbas.m	|- M = ( freeMnd ` I )
2		frmdbas.b	|- B = ( Base ` M )
3		id	|- ( X e. B -> X e. B )
4	1 2	elbasfv	|- ( X e. B -> I e. _V )
5	1 2	frmdbas	|- ( I e. _V -> B = Word I )
6	4 5	syl	|- ( X e. B -> B = Word I )
7	3 6	eleqtrd	|- ( X e. B -> X e. Word I )