Theorem brparts

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

	Ref	Expression
Assertion	brparts	$$⊢A\in V\to \left(R\mathrm{Parts}A\leftrightarrow \left(R\in \mathrm{Disjs}\wedge R\mathrm{DomainQss}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-parts	$$⊢\mathrm{Parts}={\mathrm{DomainQss}\upharpoonright }_{\mathrm{Disjs}}$$
2	1	eqres	$$⊢A\in V\to \left(R\mathrm{Parts}A\leftrightarrow \left(R\in \mathrm{Disjs}\wedge R\mathrm{DomainQss}A\right)\right)$$