Theorem unissel

Description: Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006)

	Ref	Expression
Assertion	unissel	⊢ ( ( ∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴 ) → ∪ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( ∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴 ) → ∪ 𝐴 ⊆ 𝐵 )
2		elssuni	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝐴 )
3	2	adantl	⊢ ( ( ∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ⊆ ∪ 𝐴 )
4	1 3	eqssd	⊢ ( ( ∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴 ) → ∪ 𝐴 = 𝐵 )