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 e. V -> ( 2 <_ ( # ` D ) <-> E. x e. D E. y e. D x =/= y ) )

Proof

Step Hyp Ref Expression
1 hashge2el2dif 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> E. x e. D E. y e. D x =/= y )
2 hashge2el2difr 
 |-  ( ( D e. V /\ E. x e. D E. y e. D x =/= y ) -> 2 <_ ( # ` D ) )
3 1 2 impbida 
 |-  ( D e. V -> ( 2 <_ ( # ` D ) <-> E. x e. D E. y e. D x =/= y ) )