Definition df-prt

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

	Ref	Expression
Assertion	df-prt	$$⊢\mathrm{Prt}A\leftrightarrow \forall x\in A\forall y\in A\left(x=y\vee x\cap y=\varnothing \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wprt	$$wff\mathrm{Prt}A$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4	2	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	4 5	wceq	$$wffx=y$$
7	4 5	cin	$$class\left(x\cap y\right)$$
8		c0	$$class\varnothing$$
9	7 8	wceq	$$wffx\cap y=\varnothing$$
10	6 9	wo	$$wff\left(x=y\vee x\cap y=\varnothing \right)$$
11	10 3 0	wral	$$wff\forall y\in A\left(x=y\vee x\cap y=\varnothing \right)$$
12	11 2 0	wral	$$wff\forall x\in A\forall y\in A\left(x=y\vee x\cap y=\varnothing \right)$$
13	1 12	wb	$$wff\left(\mathrm{Prt}A\leftrightarrow \forall x\in A\forall y\in A\left(x=y\vee x\cap y=\varnothing \right)\right)$$