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

Metamath Proof Explorer

Theorem unissel

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

Ref Expression
Assertion unissel ⊢ ⋃ A ⊆ B ∧ B ∈ A → ⋃ A = B

Proof

Step Hyp Ref Expression
1 simpl ⊢ ⋃ A ⊆ B ∧ B ∈ A → ⋃ A ⊆ B
2 elssuni ⊢ B ∈ A → B ⊆ ⋃ A
3 2 adantl ⊢ ⋃ A ⊆ B ∧ B ∈ A → B ⊆ ⋃ A
4 1 3 eqssd ⊢ ⋃ A ⊆ B ∧ B ∈ A → ⋃ A = B