Definition df-div 5672

Description: Define division. Theorem divmul 5674 relates it to multiplication, and divcl 5679 and redivcl 5754 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:   x,y,z,w

Detailed syntax breakdown of Definition df-div

Step	Hyp	Ref	Expression
1		cdiv 5266	. 2 class /
2		vx	. . . . . . 7 set x
3	2	cv 952	. . . . . 6 class x
4		cc 5204	. . . . . 6 class CC
5	3, 4	wcel 955	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 952	. . . . . 6 class y
8		cc0 5206	. . . . . . . 8 class 0
9	8	csn 2399	. . . . . . 7 class {0}
10	4, 9	cdif 2034	. . . . . 6 class (CC \ {0})
11	7, 10	wcel 955	. . . . 5 wff y e. (CC \ {0})
12	5, 11	wa 223	. . . 4 wff (x e. CC /\ y e. (CC \ {0}))
13		vz	. . . . . 6 set z
14	13	cv 952	. . . . 5 class z
15		vw	. . . . . . . . . 10 set w
16	15	cv 952	. . . . . . . . 9 class w
17		cmul 5211	. . . . . . . . 9 class x.
18	7, 16, 17	co 3948	. . . . . . . 8 class (y x. w)
19	18, 3	wceq 953	. . . . . . 7 wff (y x. w) = x
20	19, 15, 4	crab 1640	. . . . . 6 class {w e. CC | (y x. w) = x}
21	20	cuni 2493	. . . . 5 class U.{w e. CC | (y x. w) = x}
22	14, 21	wceq 953	. . . 4 wff z = U.{w e. CC | (y x. w) = x}
23	12, 22	wa 223	. . 3 wff ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})
24	23, 2, 6, 13	copab2 3949	. 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 953	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 5673

Copyright terms: Public domain