Metamath Proof Explorer


Theorem neq0

Description: A class is not empty if and only if it has at least one element. Proposition 5.17(1) of TakeutiZaring p. 20. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion neq0 ¬ A = x x A

Proof

Step Hyp Ref Expression
1 nfcv _ x A
2 1 neq0f ¬ A = x x A