This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssuniint

Description: Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses ssuniint.x ⊢ Ⅎ x φ
ssuniint.a ⊢ φ → A ∈ V
ssuniint.b ⊢ φ ∧ x ∈ B → A ∈ x
Assertion ssuniint ⊢ φ → A ⊆ ⋃ ⋂ B

Proof

Step Hyp Ref Expression
1 ssuniint.x ⊢ Ⅎ x φ
2 ssuniint.a ⊢ φ → A ∈ V
3 ssuniint.b ⊢ φ ∧ x ∈ B → A ∈ x
4 1 2 3 elintd ⊢ φ → A ∈ ⋂ B
5 elssuni ⊢ A ∈ ⋂ B → A ⊆ ⋃ ⋂ B
6 4 5 syl ⊢ φ → A ⊆ ⋃ ⋂ B