Theorem bnj923

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj923.1	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
Assertion	bnj923	$$⊢n\in D\to n\in \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		bnj923.1	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
2		eldifi	$$⊢n\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\to n\in \mathrm{\omega }$$
3	2 1	eleq2s	$$⊢n\in D\to n\in \mathrm{\omega }$$