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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0fin | ||
2 | eleq1 | ||
3 | 1 2 | mpbiri | |
4 | 3 | con3i | |
5 | neq0 | ||
6 | 4 5 | sylib |