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 e. Rels | A. u A. v A. x ( ( u r x /\ v r x ) -> u = v ) }

Proof

Step Hyp Ref Expression
1 dfdisjs2 
 |-  Disjs = { r e. Rels | ,~ `' r C_ _I }
2 cosscnvssid3 
 |-  ( ,~ `' r C_ _I <-> A. u A. v A. x ( ( u r x /\ v r x ) -> u = v ) )
3 1 2 rabbieq 
 |-  Disjs = { r e. Rels | A. u A. v A. x ( ( u r x /\ v r x ) -> u = v ) }