Theorem n0f

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	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eq0f.1	⊢ Ⅎ 𝑥 𝐴
2		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
3	1	neq0f	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
4	2 3	bitri	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )