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	⊢ ( 𝐷 ∈ 𝑉 → ( 2 ≤ ( ♯ ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		hashge2el2dif	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 )
2		hashge2el2difr	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ) → 2 ≤ ( ♯ ‘ 𝐷 ) )
3	1 2	impbida	⊢ ( 𝐷 ∈ 𝑉 → ( 2 ≤ ( ♯ ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ) )