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\in V\to \left(2\le \left|D\right|\leftrightarrow \exists x\in D\exists y\in Dx\ne y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashge2el2dif	$$⊢\left(D\in V\wedge 2\le \left|D\right|\right)\to \exists x\in D\exists y\in Dx\ne y$$
2		hashge2el2difr	$$⊢\left(D\in V\wedge \exists x\in D\exists y\in Dx\ne y\right)\to 2\le \left|D\right|$$
3	1 2	impbida	$$⊢D\in V\to \left(2\le \left|D\right|\leftrightarrow \exists x\in D\exists y\in Dx\ne y\right)$$