Theorem uniin

Description: The class union of the intersection of two classes. Exercise 4.12(n) of Mendelson p. 235. See uniinqs for a condition where equality holds. (Contributed by NM, 4-Dec-2003) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	uniin	|- U. ( A i^i B ) C_ ( U. A i^i U. B )

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( A i^i B ) C_ A
2	1	unissi	|- U. ( A i^i B ) C_ U. A
3		inss2	|- ( A i^i B ) C_ B
4	3	unissi	|- U. ( A i^i B ) C_ U. B
5	2 4	ssini	|- U. ( A i^i B ) C_ ( U. A i^i U. B )