Metamath Proof Explorer


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 A⊔︀B=×A1𝑜×B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA classA
1 cB classB
2 0 1 cdju classA⊔︀B
3 c0 class
4 3 csn class
5 4 0 cxp class×A
6 c1o class1𝑜
7 6 csn class1𝑜
8 7 1 cxp class1𝑜×B
9 5 8 cun class×A1𝑜×B
10 2 9 wceq wffA⊔︀B=×A1𝑜×B