Theorem brparts2

Description: Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021)

	Ref	Expression
Assertion	brparts2	|- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ ( dom R /. R ) = A ) ) )

Proof

Step	Hyp	Ref	Expression
1		brparts	|- ( A e. V -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) )
2	1	adantr	|- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) )
3		brdmqss	|- ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> ( dom R /. R ) = A ) )
4	3	anbi2d	|- ( ( A e. V /\ R e. W ) -> ( ( R e. Disjs /\ R DomainQss A ) <-> ( R e. Disjs /\ ( dom R /. R ) = A ) ) )
5	2 4	bitrd	|- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> ( R e. Disjs /\ ( dom R /. R ) = A ) ) )