Definition df-bj-tag 32963

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.)

Assertion

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

Detailed syntax breakdown of Definition df-bj-tag

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	bj-ctag 32962	. 2 class tag A
3	1	bj-csngl 32953	. . 3 class sngl A
4		c0 3915	. . . 4 class (/)
5	4	csn 4177	. . 3 class { (/) }
6	3, 5	cun 3572	. 2 class (sngl A u. { (/) } )
7	2, 6	wceq 1483	1 wff tag A = (sngl A u. { (/) } )

This definition is referenced by:  bj-tageq  32964  bj-eltag  32965  bj-0eltag  32966  bj-tagss  32968  bj-snglsstag  32969  bj-sngltag  32971  bj-tagex  32975