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 )