Definition df-part 36980

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

Assertion

Ref	Expression
df-part	⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))

Detailed syntax breakdown of Definition df-part

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wpart 36420	. 2 wff 𝑅 Part 𝐴
4	2	wdisjALTV 36415	. . 3 wff Disj 𝑅
5	1, 2	wdmqs 36405	. . 3 wff 𝑅 DomainQs 𝐴
6	4, 5	wa 397	. 2 wff ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴)
7	3, 6	wb 205	1 wff (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))

This definition is referenced by:  dfpart2  36983  dfmembpart2  36984  brpartspart  36987