Metamath Proof Explorer

Theorem brparts

Description: Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021)

Ref Expression
Assertion brparts 
|- ( A e. V -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) )

Proof

Step Hyp Ref Expression
1 df-parts 
 |-  Parts = ( DomainQss |` Disjs )
2 1 eqres 
 |-  ( A e. V -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) )