df-prt

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

		Ref	Expression
	Assertion	df-prt	$⊢ Prt A \leftrightarrow \forall x \in A \forall y \in A (x = y \lor x \cap y = \emptyset)$

Step	Hyp	Ref	Expression
0		cA	$class A$
1	0	wprt	$wff Prt A$
2		vx	$setvar x$
3		vy	$setvar y$
4	2	cv	$setvar x$
5	3	cv	$setvar y$
6	4 5	wceq	$wff x = y$
7	4 5	cin	$class (x \cap y)$
8		c0	$class \emptyset$
9	7 8	wceq	$wff x \cap y = \emptyset$
10	6 9	wo	$wff (x = y \lor x \cap y = \emptyset)$
11	10 3 0	wral	$wff \forall y \in A (x = y \lor x \cap y = \emptyset)$
12	11 2 0	wral	$wff \forall x \in A \forall y \in A (x = y \lor x \cap y = \emptyset)$
13	1 12	wb	$wff (Prt A \leftrightarrow \forall x \in A \forall y \in A (x = y \lor x \cap y = \emptyset))$

Metamath Proof Explorer