Theorem iunss2

Description: A subclass condition on the members of two indexed classes C ( x ) and D ( y ) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of TakeutiZaring p. 59. Compare uniss2 . (Contributed by NM, 9-Dec-2004)

	Ref	Expression
Assertion	iunss2	|- ( A. x e. A E. y e. B C C_ D -> U_ x e. A C C_ U_ y e. B D )

Proof

Step	Hyp	Ref	Expression
1		ssiun	|- ( E. y e. B C C_ D -> C C_ U_ y e. B D )
2	1	ralimi	|- ( A. x e. A E. y e. B C C_ D -> A. x e. A C C_ U_ y e. B D )
3		iunss	|- ( U_ x e. A C C_ U_ y e. B D <-> A. x e. A C C_ U_ y e. B D )
4	2 3	sylibr	|- ( A. x e. A E. y e. B C C_ D -> U_ x e. A C C_ U_ y e. B D )