Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Disjoints vs. converse functions
disjrel
Next ⟩
disjss
Metamath Proof Explorer
Ascii
Unicode
Theorem
disjrel
Description:
Disjoint relation is a relation.
(Contributed by
Peter Mazsa
, 15-Sep-2021)
Ref
Expression
Assertion
disjrel
⊢
Disj
R
→
Rel
⁡
R
Proof
Step
Hyp
Ref
Expression
1
df-disjALTV
⊢
Disj
R
↔
CnvRefRel
≀
R
-1
∧
Rel
⁡
R
2
1
simprbi
⊢
Disj
R
→
Rel
⁡
R