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	Could not format assertion : No typesetting found for |- ( R Part A <-> ( Disj R /\ R DomainQs A ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wpart	Could not format R Part A : No typesetting found for wff R Part A with typecode wff
3	0	wdisjALTV	$$wffDisjR$$
4	1 0	wdmqs	$$wffRDomainQsA$$
5	3 4	wa	$$wff\left(DisjR\wedge RDomainQsA\right)$$
6	2 5	wb	Could not format ( R Part A <-> ( Disj R /\ R DomainQs A ) ) : No typesetting found for wff ( R Part A <-> ( Disj R /\ R DomainQs A ) ) with typecode wff