Metamath Proof Explorer


Theorem djuex

Description: The disjoint union of sets is a set. For a shorter proof using djuss see djuexALT . (Contributed by AV, 28-Jun-2022)

Ref Expression
Assertion djuex AVBWA⊔︀BV

Proof

Step Hyp Ref Expression
1 df-dju A⊔︀B=×A1𝑜×B
2 snex V
3 2 a1i BWV
4 xpexg VAV×AV
5 3 4 sylan BWAV×AV
6 5 ancoms AVBW×AV
7 snex 1𝑜V
8 7 a1i AV1𝑜V
9 xpexg 1𝑜VBW1𝑜×BV
10 8 9 sylan AVBW1𝑜×BV
11 unexg ×AV1𝑜×BV×A1𝑜×BV
12 6 10 11 syl2anc AVBW×A1𝑜×BV
13 1 12 eqeltrid AVBWA⊔︀BV