Theorem bj-sngltagi

Description: The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sngltagi	$$⊢A\in snglB\to A\in tagB$$

Proof

Step	Hyp	Ref	Expression
1		bj-snglsstag	$$⊢snglB\subseteq tagB$$
2	1	sseli	$$⊢A\in snglB\to A\in tagB$$