Theorem epn0

Description: The membership relation is nonempty. (Contributed by AV, 19-Jun-2022)

	Ref	Expression
Assertion	epn0	$$⊢\mathrm{E}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0sn0ep	$$⊢\varnothing \mathrm{E}\left\{\varnothing \right\}$$
2		brne0	$$⊢\varnothing \mathrm{E}\left\{\varnothing \right\}\to \mathrm{E}\ne \varnothing$$
3	1 2	ax-mp	$$⊢\mathrm{E}\ne \varnothing$$