Theorem bj-eltag

Description: Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-eltag	|- ( A e. tag B <-> ( E. x e. B A = { x } \/ A = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-tag	|- tag B = ( sngl B u. { (/) } )
2	1	eleq2i	|- ( A e. tag B <-> A e. ( sngl B u. { (/) } ) )
3		elun	|- ( A e. ( sngl B u. { (/) } ) <-> ( A e. sngl B \/ A e. { (/) } ) )
4		bj-elsngl	|- ( A e. sngl B <-> E. x e. B A = { x } )
5		0ex	|- (/) e. _V
6	5	elsn2	|- ( A e. { (/) } <-> A = (/) )
7	4 6	orbi12i	|- ( ( A e. sngl B \/ A e. { (/) } ) <-> ( E. x e. B A = { x } \/ A = (/) ) )
8	2 3 7	3bitri	|- ( A e. tag B <-> ( E. x e. B A = { x } \/ A = (/) ) )