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

Metamath Proof Explorer

Theorem intmin

Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion intmin ⊢ A ∈ B → ⋂ x ∈ B | A ⊆ x = A

Proof

Step Hyp Ref Expression
1 vex ⊢ y ∈ V
2 1 elintrab ⊢ y ∈ ⋂ x ∈ B | A ⊆ x ↔ ∀ x ∈ B A ⊆ x → y ∈ x
3 ssid ⊢ A ⊆ A
4 sseq2 ⊢ x = A → A ⊆ x ↔ A ⊆ A
5 eleq2 ⊢ x = A → y ∈ x ↔ y ∈ A
6 4 5 imbi12d ⊢ x = A → A ⊆ x → y ∈ x ↔ A ⊆ A → y ∈ A
7 6 rspcv ⊢ A ∈ B → ∀ x ∈ B A ⊆ x → y ∈ x → A ⊆ A → y ∈ A
8 3 7 mpii ⊢ A ∈ B → ∀ x ∈ B A ⊆ x → y ∈ x → y ∈ A
9 2 8 biimtrid ⊢ A ∈ B → y ∈ ⋂ x ∈ B | A ⊆ x → y ∈ A
10 9 ssrdv ⊢ A ∈ B → ⋂ x ∈ B | A ⊆ x ⊆ A
11 ssintub ⊢ A ⊆ ⋂ x ∈ B | A ⊆ x
12 11 a1i ⊢ A ∈ B → A ⊆ ⋂ x ∈ B | A ⊆ x
13 10 12 eqssd ⊢ A ∈ B → ⋂ x ∈ B | A ⊆ x = A