Theorem bj-disjsn01

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

	Ref	Expression
Assertion	bj-disjsn01	⊢ ( { ∅ } ∩ { 1o } ) = ∅

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	necomi	⊢ ∅ ≠ 1o
3		disjsn2	⊢ ( ∅ ≠ 1o → ( { ∅ } ∩ { 1o } ) = ∅ )
4	2 3	ax-mp	⊢ ( { ∅ } ∩ { 1o } ) = ∅