This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjALTVid

Description: The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021)

		Ref	Expression
	Assertion	disjALTVid	⊢ Disj I

Step	Hyp	Ref	Expression
1		cosscnvid	⊢ ≀ ^◡ I = I
2	1	eqimssi	⊢ ≀ ^◡ I ⊆ I
3		reli	⊢ Rel I
4		dfdisjALTV2	⊢ ( Disj I ↔ ( ≀ ^◡ I ⊆ I ∧ Rel I ) )
5	2 3 4	mpbir2an	⊢ Disj I