Definition df-prt

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

	Ref	Expression
Assertion	df-prt	|- ( Prt A <-> A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	wprt	|- Prt A
2		vx	|- x
3		vy	|- y
4	2	cv	|- x
5	3	cv	|- y
6	4 5	wceq	|- x = y
7	4 5	cin	|- ( x i^i y )
8		c0	|- (/)
9	7 8	wceq	|- ( x i^i y ) = (/)
10	6 9	wo	|- ( x = y \/ ( x i^i y ) = (/) )
11	10 3 0	wral	|- A. y e. A ( x = y \/ ( x i^i y ) = (/) )
12	11 2 0	wral	|- A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) )
13	1 12	wb	|- ( Prt A <-> A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) ) )