Theorem bj-tagci

Description: Characterization of the elements of B in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-tagci	$$⊢A\in B\to \left\{A\right\}\in tagB$$

Proof

Step	Hyp	Ref	Expression
1		bj-snglc	$$⊢A\in B\leftrightarrow \left\{A\right\}\in snglB$$
2		bj-sngltagi	$$⊢\left\{A\right\}\in snglB\to \left\{A\right\}\in tagB$$
3	1 2	sylbi	$$⊢A\in B\to \left\{A\right\}\in tagB$$