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	⊢ ∪ ( 𝐴 ∩ 𝐵 ) ⊆ ( ∪ 𝐴 ∩ ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
2	1	unissi	⊢ ∪ ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝐴
3		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
4	3	unissi	⊢ ∪ ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝐵
5	2 4	ssini	⊢ ∪ ( 𝐴 ∩ 𝐵 ) ⊆ ( ∪ 𝐴 ∩ ∪ 𝐵 )