Theorem wrddun

Description: Words in either of two alphabets are words in their union. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	wrddun	|- ( ( A e. Word B \/ A e. Word C ) -> A e. Word ( B u. C ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- B C_ ( B u. C )
2		sswrd	|- ( B C_ ( B u. C ) -> Word B C_ Word ( B u. C ) )
3	1 2	ax-mp	|- Word B C_ Word ( B u. C )
4	3	sseli	|- ( A e. Word B -> A e. Word ( B u. C ) )
5		ssun2	|- C C_ ( B u. C )
6		sswrd	|- ( C C_ ( B u. C ) -> Word C C_ Word ( B u. C ) )
7	5 6	ax-mp	|- Word C C_ Word ( B u. C )
8	7	sseli	|- ( A e. Word C -> A e. Word ( B u. C ) )
9	4 8	jaoi	|- ( ( A e. Word B \/ A e. Word C ) -> A e. Word ( B u. C ) )