Definition df-prt 34157

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

Assertion

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

Distinct variable group:   x, y, A

Detailed syntax breakdown of Definition df-prt

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wprt 34156	. 2 wff Prt A
3		vx	. . . . . 6 setvar x
4		vy	. . . . . 6 setvar y
5	3, 4	weq 1874	. . . . 5 wff x = y
6	3	cv 1482	. . . . . . 7 class x
7	4	cv 1482	. . . . . . 7 class y
8	6, 7	cin 3573	. . . . . 6 class ( x i^i y )
9		c0 3915	. . . . . 6 class (/)
10	8, 9	wceq 1483	. . . . 5 wff ( x i^i y ) = (/)
11	5, 10	wo 383	. . . 4 wff ( x = y \/ ( x i^i y ) = (/) )
12	11, 4, 1	wral 2912	. . 3 wff A. y e. A ( x = y \/ ( x i^i y ) = (/) )
13	12, 3, 1	wral 2912	. 2 wff A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) )
14	2, 13	wb 196	1 wff ( Prt A <-> A. x e. A A. y e. A ( x = y \/ ( x i^i y ) = (/) ) )

This definition is referenced by:  erprt  34158  prtlem14  34159