This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjimres

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

Ref Expression
Assertion disjimres ( Disj 𝑅 → Disj ( 𝑅 ↾ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 resss ⊢ ( 𝑅 ↾ 𝐴 ) ⊆ 𝑅
2 1 disjssi ⊢ ( Disj 𝑅 → Disj ( 𝑅 ↾ 𝐴 ) )