Definition df-prt 38873

Description: Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)

Assertion

Ref	Expression
df-prt	⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))

Distinct variable group:   𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-prt

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wprt 38872	. 2 wff Prt 𝐴
3		vx	. . . . . 6 setvar 𝑥
4		vy	. . . . . 6 setvar 𝑦
5	3, 4	weq 1962	. . . . 5 wff 𝑥 = 𝑦
6	3	cv 1539	. . . . . . 7 class 𝑥
7	4	cv 1539	. . . . . . 7 class 𝑦
8	6, 7	cin 3950	. . . . . 6 class (𝑥 ∩ 𝑦)
9		c0 4333	. . . . . 6 class ∅
10	8, 9	wceq 1540	. . . . 5 wff (𝑥 ∩ 𝑦) = ∅
11	5, 10	wo 848	. . . 4 wff (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)
12	11, 4, 1	wral 3061	. . 3 wff ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)
13	12, 3, 1	wral 3061	. 2 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)
14	2, 13	wb 206	1 wff (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))

This definition is referenced by:  erprt  38874  prtlem14  38875