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

Metamath Proof Explorer

Theorem unimax

Description: Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002)

Ref Expression
Assertion unimax ⊢ A ∈ B → ⋃ x ∈ B | x ⊆ A = A

Proof

Step Hyp Ref Expression
1 ssid ⊢ A ⊆ A
2 sseq1 ⊢ x = A → x ⊆ A ↔ A ⊆ A
3 2 elrab3 ⊢ A ∈ B → A ∈ x ∈ B | x ⊆ A ↔ A ⊆ A
4 1 3 mpbiri ⊢ A ∈ B → A ∈ x ∈ B | x ⊆ A
5 sseq1 ⊢ x = y → x ⊆ A ↔ y ⊆ A
6 5 elrab ⊢ y ∈ x ∈ B | x ⊆ A ↔ y ∈ B ∧ y ⊆ A
7 6 simprbi ⊢ y ∈ x ∈ B | x ⊆ A → y ⊆ A
8 7 rgen ⊢ ∀ y ∈ x ∈ B | x ⊆ A y ⊆ A
9 ssunieq ⊢ A ∈ x ∈ B | x ⊆ A ∧ ∀ y ∈ x ∈ B | x ⊆ A y ⊆ A → A = ⋃ x ∈ B | x ⊆ A
10 9 eqcomd ⊢ A ∈ x ∈ B | x ⊆ A ∧ ∀ y ∈ x ∈ B | x ⊆ A y ⊆ A → ⋃ x ∈ B | x ⊆ A = A
11 4 8 10 sylancl ⊢ A ∈ B → ⋃ x ∈ B | x ⊆ A = A