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 }