# Metamath Proof Explorer

## Theorem djuexb

Description: The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023)

Ref Expression
Assertion djuexb
`|- ( ( A e. _V /\ B e. _V ) <-> ( A |_| B ) e. _V )`

### Proof

Step Hyp Ref Expression
1 djuex
` |-  ( ( A e. _V /\ B e. _V ) -> ( A |_| B ) e. _V )`
2 df-dju
` |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )`
3 2 eleq1i
` |-  ( ( A |_| B ) e. _V <-> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) e. _V )`
4 unexb
` |-  ( ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) <-> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) e. _V )`
5 3 4 bitr4i
` |-  ( ( A |_| B ) e. _V <-> ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) )`
6 0nep0
` |-  (/) =/= { (/) }`
7 6 necomi
` |-  { (/) } =/= (/)`
8 rnexg
` |-  ( ( { (/) } X. A ) e. _V -> ran ( { (/) } X. A ) e. _V )`
9 rnxp
` |-  ( { (/) } =/= (/) -> ran ( { (/) } X. A ) = A )`
10 9 eleq1d
` |-  ( { (/) } =/= (/) -> ( ran ( { (/) } X. A ) e. _V <-> A e. _V ) )`
11 8 10 syl5ib
` |-  ( { (/) } =/= (/) -> ( ( { (/) } X. A ) e. _V -> A e. _V ) )`
12 7 11 ax-mp
` |-  ( ( { (/) } X. A ) e. _V -> A e. _V )`
13 1oex
` |-  1o e. _V`
14 13 snnz
` |-  { 1o } =/= (/)`
15 rnexg
` |-  ( ( { 1o } X. B ) e. _V -> ran ( { 1o } X. B ) e. _V )`
16 rnxp
` |-  ( { 1o } =/= (/) -> ran ( { 1o } X. B ) = B )`
17 16 eleq1d
` |-  ( { 1o } =/= (/) -> ( ran ( { 1o } X. B ) e. _V <-> B e. _V ) )`
18 15 17 syl5ib
` |-  ( { 1o } =/= (/) -> ( ( { 1o } X. B ) e. _V -> B e. _V ) )`
19 14 18 ax-mp
` |-  ( ( { 1o } X. B ) e. _V -> B e. _V )`
20 12 19 anim12i
` |-  ( ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) -> ( A e. _V /\ B e. _V ) )`
21 5 20 sylbi
` |-  ( ( A |_| B ) e. _V -> ( A e. _V /\ B e. _V ) )`
22 1 21 impbii
` |-  ( ( A e. _V /\ B e. _V ) <-> ( A |_| B ) e. _V )`