Theorem bj-sngltag

Description: The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sngltag	|- ( A e. V -> ( { A } e. sngl B <-> { A } e. tag B ) )

Proof

Step	Hyp	Ref	Expression
1		bj-sngltagi	|- ( { A } e. sngl B -> { A } e. tag B )
2		df-bj-tag	|- tag B = ( sngl B u. { (/) } )
3	2	eleq2i	|- ( { A } e. tag B <-> { A } e. ( sngl B u. { (/) } ) )
4		elun	|- ( { A } e. ( sngl B u. { (/) } ) <-> ( { A } e. sngl B \/ { A } e. { (/) } ) )
5		idd	|- ( A e. V -> ( { A } e. sngl B -> { A } e. sngl B ) )
6		elsni	|- ( { A } e. { (/) } -> { A } = (/) )
7		snprc	|- ( -. A e. _V <-> { A } = (/) )
8		elex	|- ( A e. V -> A e. _V )
9	8	pm2.24d	|- ( A e. V -> ( -. A e. _V -> { A } e. sngl B ) )
10	7 9	syl5bir	|- ( A e. V -> ( { A } = (/) -> { A } e. sngl B ) )
11	6 10	syl5	|- ( A e. V -> ( { A } e. { (/) } -> { A } e. sngl B ) )
12	5 11	jaod	|- ( A e. V -> ( ( { A } e. sngl B \/ { A } e. { (/) } ) -> { A } e. sngl B ) )
13	4 12	syl5bi	|- ( A e. V -> ( { A } e. ( sngl B u. { (/) } ) -> { A } e. sngl B ) )
14	3 13	syl5bi	|- ( A e. V -> ( { A } e. tag B -> { A } e. sngl B ) )
15	1 14	impbid2	|- ( A e. V -> ( { A } e. sngl B <-> { A } e. tag B ) )