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	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj923	⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		bnj923.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
2		eldifi	⊢ ( 𝑛 ∈ ( ω ∖ { ∅ } ) → 𝑛 ∈ ω )
3	2 1	eleq2s	⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )