Definition df-bj-tag 36936

Description: Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) 𝐴 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 𝐴 = (sngl 𝐴 ∪ {∅})

Detailed syntax breakdown of Definition df-bj-tag

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	bj-ctag 36935	. 2 class tag 𝐴
3	1	bj-csngl 36926	. . 3 class sngl 𝐴
4		c0 4292	. . . 4 class ∅
5	4	csn 4585	. . 3 class {∅}
6	3, 5	cun 3909	. 2 class (sngl 𝐴 ∪ {∅})
7	2, 6	wceq 1540	1 wff tag 𝐴 = (sngl 𝐴 ∪ {∅})

This definition is referenced by:  bj-tageq  36937  bj-eltag  36938  bj-0eltag  36939  bj-tagss  36941  bj-snglsstag  36942  bj-sngltag  36944  bj-tagex  36948