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