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

Proof

Step Hyp Ref Expression
1 cosscnvid 
 |-  ,~ `' _I = _I
2 1 eqimssi 
 |-  ,~ `' _I C_ _I
3 reli 
 |-  Rel _I
4 dfdisjALTV2 
 |-  ( Disj _I <-> ( ,~ `' _I C_ _I /\ Rel _I ) )
5 2 3 4 mpbir2an 
 |-  Disj _I