Theorem bj-disjsn01

Description: Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-disjsn01	$$⊢\left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2	1	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
3		disjsn2	$$⊢\varnothing \ne 1_{𝑜}\to \left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$
4	2 3	ax-mp	$$⊢\left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$