df-dvds

Description: Define the divides relation, see definition in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	df-dvds	$⊢ ∥ = \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\}$

Step	Hyp	Ref	Expression
0		cdvds	$class ∥$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cz	$class ℤ$
5	3 4	wcel	$wff x \in ℤ$
6	2	cv	$setvar y$
7	6 4	wcel	$wff y \in ℤ$
8	5 7	wa	$wff (x \in ℤ \land y \in ℤ)$
9		vn	$setvar n$
10	9	cv	$setvar n$
11		cmul	$class \times$
12	10 3 11	co	$class n x$
13	12 6	wceq	$wff n x = y$
14	13 9 4	wrex	$wff \exists n \in ℤ n x = y$
15	8 14	wa	$wff ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)$
16	15 1 2	copab	$class \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\}$
17	0 16	wceq	$wff ∥ = \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists n \in ℤ n x = y)\}$

Metamath Proof Explorer