Definition df-div 4216

Description: Define division. Theorem divmul 4218 relates it to multiplication, and divcl 4221 and redivcl 4274 prove its closure laws.

Assertion

Ref	Expression
df-div	|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})}

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Definition df-div

Step	Hyp	Ref	Expression
1		cdiv 4091	. 2 class /
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cc 4026	. . . . . 6 class CC
5	3, 4	wcel 1092	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8		cc0 4028	. . . . . . . 8 class 0
9	8	csn 1808	. . . . . . 7 class {0}
10	4, 9	cdif 1484	. . . . . 6 class (CC \ {0})
11	7, 10	wcel 1092	. . . . 5 wff y e. (CC \ {0})
12	5, 11	wa 196	. . . 4 wff (x e. CC /\ y e. (CC \ {0}))
13		vz	. . . . . 6 set z
14	13	cv 1089	. . . . 5 class z
15		vw	. . . . . . . . . 10 set w
16	15	cv 1089	. . . . . . . . 9 class w
17		cmulc 4032	. . . . . . . . 9 class x.
18	7, 16, 17	co 3001	. . . . . . . 8 class (y x. w)
19	18, 3	wceq 1091	. . . . . . 7 wff (y x. w) = x
20	19, 15, 4	crab 1204	. . . . . 6 class {w e. CC | (y x. w) = x}
21	20	cuni 1919	. . . . 5 class U.{w e. CC | (y x. w) = x}
22	14, 21	wceq 1091	. . . 4 wff z = U.{w e. CC | (y x. w) = x}
23	12, 22	wa 196	. . 3 wff ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})
24	23, 2, 6, 13	copab2 3002	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})}
25	1, 24	wceq 1091	1 wff / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})}

This definition is referenced by:  divval 4217

metamath.org