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 Fin x x A

Proof

Step Hyp Ref Expression
1 0fin Fin
2 eleq1 A = A Fin Fin
3 1 2 mpbiri A = A Fin
4 3 con3i ¬ A Fin ¬ A =
5 neq0 ¬ A = x x A
6 4 5 sylib ¬ A Fin x x A