Description: A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of TakeutiZaring p. 20. This version of n0 requires only that x not be free in, rather than not occur in, A . (Contributed by NM, 17-Oct-2003)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eq0f.1 | |
|
Assertion | n0f | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eq0f.1 | |
|
2 | df-ne | |
|
3 | 1 | neq0f | |
4 | 2 3 | bitri | |