Metamath Proof Explorer


Theorem disjALTVidres

Description: The class of identity relations restricted is disjoint. (Contributed by Peter Mazsa, 28-Jun-2020) (Revised by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion disjALTVidres
|- Disj ( _I |` A )

Proof

Step Hyp Ref Expression
1 disjALTVid
 |-  Disj _I
2 disjimres
 |-  ( Disj _I -> Disj ( _I |` A ) )
3 1 2 ax-mp
 |-  Disj ( _I |` A )