Theorem ssuni

Description: Subclass relationship for class union. (Contributed by NM, 24-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	ssuni	|- ( ( A C_ B /\ B e. C ) -> A C_ U. C )

Proof

Step	Hyp	Ref	Expression
1		elunii	|- ( ( x e. B /\ B e. C ) -> x e. U. C )
2	1	expcom	|- ( B e. C -> ( x e. B -> x e. U. C ) )
3	2	imim2d	|- ( B e. C -> ( ( x e. A -> x e. B ) -> ( x e. A -> x e. U. C ) ) )
4	3	alimdv	|- ( B e. C -> ( A. x ( x e. A -> x e. B ) -> A. x ( x e. A -> x e. U. C ) ) )
5		df-ss	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
6		df-ss	|- ( A C_ U. C <-> A. x ( x e. A -> x e. U. C ) )
7	4 5 6	3imtr4g	|- ( B e. C -> ( A C_ B -> A C_ U. C ) )
8	7	impcom	|- ( ( A C_ B /\ B e. C ) -> A C_ U. C )