Theorem bj-n0i

Description: Inference associated with n0 . Shortens 2ndcdisj (2888>2878), notsep (264>253). (Contributed by BJ, 22-Apr-2019)

	Ref	Expression
Hypothesis	bj-n0i.1	$$⊢A\ne \varnothing$$
Assertion	bj-n0i	$$⊢\exists xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		bj-n0i.1	$$⊢A\ne \varnothing$$
2		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
3	1 2	mpbi	$$⊢\exists xx\in A$$