Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Disjoints vs. converse functions
disjimres
Next ⟩
disjimin
Metamath Proof Explorer
Ascii
Unicode
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