Metamath Proof Explorer


Theorem disjALTVxrnidres

Description: The class of range Cartesian product with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 25-Jun-2020) (Revised by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion disjALTVxrnidres
|- Disj ( R |X. ( _I |` A ) )

Proof

Step Hyp Ref Expression
1 disjALTVid
 |-  Disj _I
2 disjimxrnres
 |-  ( Disj _I -> Disj ( R |X. ( _I |` A ) ) )
3 1 2 ax-mp
 |-  Disj ( R |X. ( _I |` A ) )