Theorem unissi

Description: Subclass relationship for subclass union. Inference form of uniss . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypothesis	unissi.1	|- A C_ B
Assertion	unissi	|- U. A C_ U. B

Proof

Step	Hyp	Ref	Expression
1		unissi.1	|- A C_ B
2		uniss	|- ( A C_ B -> U. A C_ U. B )
3	1 2	ax-mp	|- U. A C_ U. B