Metamath Proof Explorer


Theorem dfdisjs3

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

Ref Expression
Assertion dfdisjs3 Disjs = r Rels | u v x u r x v r x u = v

Proof

Step Hyp Ref Expression
1 dfdisjs2 Disjs = r Rels | r -1 I
2 cosscnvssid3 r -1 I u v x u r x v r x u = v
3 1 2 rabbieq Disjs = r Rels | u v x u r x v r x u = v