This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ R Part A \leftrightarrow (Disj R \land R DomainQs A)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2	1 0	wpart	$wff R Part A$
3	0	wdisjALTV	$wff Disj R$
4	1 0	wdmqs	$wff R DomainQs A$
5	3 4	wa	$wff (Disj R \land R DomainQs A)$
6	2 5	wb	$wff (R Part A \leftrightarrow (Disj R \land R DomainQs A))$