Theorem bj-sngltagi

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

	Ref	Expression
Assertion	bj-sngltagi	⊢ ( 𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bj-snglsstag	⊢ sngl 𝐵 ⊆ tag 𝐵
2	1	sseli	⊢ ( 𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵 )