Metamath Proof Explorer


Theorem nfielex

Description: If a class is not finite, then it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018)

Ref Expression
Assertion nfielex
|- ( -. A e. Fin -> E. x x e. A )

Proof

Step Hyp Ref Expression
1 0fin
 |-  (/) e. Fin
2 eleq1
 |-  ( A = (/) -> ( A e. Fin <-> (/) e. Fin ) )
3 1 2 mpbiri
 |-  ( A = (/) -> A e. Fin )
4 3 con3i
 |-  ( -. A e. Fin -> -. A = (/) )
5 neq0
 |-  ( -. A = (/) <-> E. x x e. A )
6 4 5 sylib
 |-  ( -. A e. Fin -> E. x x e. A )