Metamath Proof Explorer

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 x A y B C D x A C y B D


Step Hyp Ref Expression
1 ssiun y B C D C y B D
2 1 ralimi x A y B C D x A C y B D
3 iunss x A C y B D x A C y B D
4 2 3 sylibr x A y B C D x A C y B D