Metamath Proof Explorer

Theorem disjALTVinidres

Description: The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion disjALTVinidres 
|- Disj ( R i^i ( _I |` A ) )

Proof

Step Hyp Ref Expression
1 disjALTVid 
 |-  Disj _I
2 disjiminres 
 |-  ( Disj _I -> Disj ( R i^i ( _I |` A ) ) )
3 1 2 ax-mp 
 |-  Disj ( R i^i ( _I |` A ) )