Theorem disjALTVid

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

	Ref	Expression
Assertion	disjALTVid	⊢ Disj I

Proof

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