Theorem bj-snglsstag

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

	Ref	Expression
Assertion	bj-snglsstag	⊢ sngl 𝐴 ⊆ tag 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ sngl 𝐴 ⊆ ( sngl 𝐴 ∪ { ∅ } )
2		df-bj-tag	⊢ tag 𝐴 = ( sngl 𝐴 ∪ { ∅ } )
3	1 2	sseqtrri	⊢ sngl 𝐴 ⊆ tag 𝐴