Definition df-prt

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wprt	⊢ Prt 𝐴
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4	2	cv	⊢ 𝑥
5	3	cv	⊢ 𝑦
6	4 5	wceq	⊢ 𝑥 = 𝑦
7	4 5	cin	⊢ ( 𝑥 ∩ 𝑦 )
8		c0	⊢ ∅
9	7 8	wceq	⊢ ( 𝑥 ∩ 𝑦 ) = ∅
10	6 9	wo	⊢ ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ )
11	10 3 0	wral	⊢ ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ )
12	11 2 0	wral	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ )
13	1 12	wb	⊢ ( Prt 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )