Theorem 0sn0ep

Description: An example for the membership relation. (Contributed by AV, 19-Jun-2022)

	Ref	Expression
Assertion	0sn0ep	$$⊢\varnothing \mathrm{E}\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2	1	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
3		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
4	3	epeli	$$⊢\varnothing \mathrm{E}\left\{\varnothing \right\}\leftrightarrow \varnothing \in \left\{\varnothing \right\}$$
5	2 4	mpbir	$$⊢\varnothing \mathrm{E}\left\{\varnothing \right\}$$