# Metamath Proof Explorer

## Theorem bnj529

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

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

### Proof

Step Hyp Ref Expression
1 bnj529.1 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
2 eldifsn ${⊢}{M}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)↔\left({M}\in \mathrm{\omega }\wedge {M}\ne \varnothing \right)$
3 2 biimpi ${⊢}{M}\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\to \left({M}\in \mathrm{\omega }\wedge {M}\ne \varnothing \right)$
4 3 1 eleq2s ${⊢}{M}\in {D}\to \left({M}\in \mathrm{\omega }\wedge {M}\ne \varnothing \right)$
5 nnord ${⊢}{M}\in \mathrm{\omega }\to \mathrm{Ord}{M}$
6 5 anim1i ${⊢}\left({M}\in \mathrm{\omega }\wedge {M}\ne \varnothing \right)\to \left(\mathrm{Ord}{M}\wedge {M}\ne \varnothing \right)$
7 ord0eln0 ${⊢}\mathrm{Ord}{M}\to \left(\varnothing \in {M}↔{M}\ne \varnothing \right)$
8 7 biimpar ${⊢}\left(\mathrm{Ord}{M}\wedge {M}\ne \varnothing \right)\to \varnothing \in {M}$
9 4 6 8 3syl ${⊢}{M}\in {D}\to \varnothing \in {M}$