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 ⊢ Ⅎ 𝑥 𝜑
ssuniint.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ssuniint.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑥 )
Assertion ssuniint ( 𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵 )

Proof

Step Hyp Ref Expression
1 ssuniint.x ⊢ Ⅎ 𝑥 𝜑
2 ssuniint.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 ssuniint.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ 𝑥 )
4 1 2 3 elintd ⊢ ( 𝜑 → 𝐴 ∈ ∩ 𝐵 )
5 elssuni ⊢ ( 𝐴 ∈ ∩ 𝐵 → 𝐴 ⊆ ∪ ∩ 𝐵 )
6 4 5 syl ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵 )