Theorem djussxp

Description: Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014)

	Ref	Expression
Assertion	djussxp	|- U_ x e. A ( { x } X. B ) C_ ( A X. _V )

Proof

Step	Hyp	Ref	Expression
1		iunss	|- ( U_ x e. A ( { x } X. B ) C_ ( A X. _V ) <-> A. x e. A ( { x } X. B ) C_ ( A X. _V ) )
2		snssi	|- ( x e. A -> { x } C_ A )
3		ssv	|- B C_ _V
4		xpss12	|- ( ( { x } C_ A /\ B C_ _V ) -> ( { x } X. B ) C_ ( A X. _V ) )
5	2 3 4	sylancl	|- ( x e. A -> ( { x } X. B ) C_ ( A X. _V ) )
6	1 5	mprgbir	|- U_ x e. A ( { x } X. B ) C_ ( A X. _V )