Metamath Proof Explorer


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 ⊢ ⋃ A ∩ B ⊆ ⋃ A ∩ ⋃ B

Proof

Step Hyp Ref Expression
1 inss1 ⊢ A ∩ B ⊆ A
2 1 unissi ⊢ ⋃ A ∩ B ⊆ ⋃ A
3 inss2 ⊢ A ∩ B ⊆ B
4 3 unissi ⊢ ⋃ A ∩ B ⊆ ⋃ B
5 2 4 ssini ⊢ ⋃ A ∩ B ⊆ ⋃ A ∩ ⋃ B