Definition df-dju

Description: Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of A or B , tagging each one with whether it came from A or B . (Contributed by Jim Kingdon, 20-Jun-2022)

	Ref	Expression
Assertion	df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cdju	$$class\left(A\mathrm{\bigsqcup ︀}B\right)$$
3		c0	$$class\varnothing$$
4	3	csn	$$class\left\{\varnothing \right\}$$
5	4 0	cxp	$$class\left(\left\{\varnothing \right\}\times A\right)$$
6		c1o	$$class{1}_{𝑜}$$
7	6	csn	$$class\left\{1_{𝑜}\right\}$$
8	7 1	cxp	$$class\left(\left\{1_{𝑜}\right\}\times B\right)$$
9	5 8	cun	$$class\left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
10	2 9	wceq	$$wff\left(A\mathrm{\bigsqcup ︀}B\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)$$