Theorem unexb

Description: Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998)

	Ref	Expression
Assertion	unexb	|- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		unexg	|- ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
2		ssun1	|- A C_ ( A u. B )
3		ssexg	|- ( ( A C_ ( A u. B ) /\ ( A u. B ) e. _V ) -> A e. _V )
4	2 3	mpan	|- ( ( A u. B ) e. _V -> A e. _V )
5		ssun2	|- B C_ ( A u. B )
6		ssexg	|- ( ( B C_ ( A u. B ) /\ ( A u. B ) e. _V ) -> B e. _V )
7	5 6	mpan	|- ( ( A u. B ) e. _V -> B e. _V )
8	4 7	jca	|- ( ( A u. B ) e. _V -> ( A e. _V /\ B e. _V ) )
9	1 8	impbii	|- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )