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

Metamath Proof Explorer

Theorem hashge2el2difb

Description: A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020)

Ref Expression
Assertion hashge2el2difb ⊢ D ∈ V → 2 ≤ D ↔ ∃ x ∈ D ∃ y ∈ D x ≠ y

Proof

Step Hyp Ref Expression
1 hashge2el2dif ⊢ D ∈ V ∧ 2 ≤ D → ∃ x ∈ D ∃ y ∈ D x ≠ y
2 hashge2el2difr ⊢ D ∈ V ∧ ∃ x ∈ D ∃ y ∈ D x ≠ y → 2 ≤ D
3 1 2 impbida ⊢ D ∈ V → 2 ≤ D ↔ ∃ x ∈ D ∃ y ∈ D x ≠ y