Metamath Proof Explorer


Theorem dfdisjs

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021)

Ref Expression
Assertion dfdisjs
|- Disjs = { r e. Rels | ,~ `' r e. CnvRefRels }

Proof

Step Hyp Ref Expression
1 df-disjs
 |-  Disjs = ( Disjss i^i Rels )
2 df-disjss
 |-  Disjss = { r | ,~ `' r e. CnvRefRels }
3 1 2 abeqin
 |-  Disjs = { r e. Rels | ,~ `' r e. CnvRefRels }