Definition df-part

Description: Define the partition predicate (read: A is a partition by R ). Alternative definition is dfpart2 . The binary partition and the partition predicate are the same if A and R are sets, cf. brpartspart . (Contributed by Peter Mazsa, 12-Aug-2021)

	Ref	Expression
Assertion	df-part	$$⊢RPartA\leftrightarrow \left(DisjR\wedge RDomainQsA\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wpart	$$wffRPartA$$
3	0	wdisjALTV	$$wffDisjR$$
4	1 0	wdmqs	$$wffRDomainQsA$$
5	3 4	wa	$$wff\left(DisjR\wedge RDomainQsA\right)$$
6	2 5	wb	$$wff\left(RPartA\leftrightarrow \left(DisjR\wedge RDomainQsA\right)\right)$$