Metamath Proof Explorer

Theorem dfdisjs4

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

Ref Expression
Assertion dfdisjs4 
|- Disjs = { r e. Rels | A. x E* u u r x }

Proof

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