Metamath Proof Explorer


Theorem disjimres

Description: Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion disjimres Disj R Disj R A

Proof

Step Hyp Ref Expression
1 resss R A R
2 1 disjssi Disj R Disj R A