Definition df-bj-tag

Description: Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) A of a disjoint element (here, the empty set). Remark: this could be used for the one-point compactification of a topological space. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	df-bj-tag	|- tag A = ( sngl A u. { (/) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	bj-ctag	|- tag A
2	0	bj-csngl	|- sngl A
3		c0	|- (/)
4	3	csn	|- { (/) }
5	2 4	cun	|- ( sngl A u. { (/) } )
6	1 5	wceq	|- tag A = ( sngl A u. { (/) } )