Definition df-div 5680

Description: Define division. Theorem divmul 5682 relates it to multiplication, and divcl 5687 and redivcl 5762 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 5274	. 2 class /
2		vx	. . . . . . 7 set x
3	2	cv 953	. . . . . 6 class x
4		cc 5212	. . . . . 6 class CC
5	3, 4	wcel 956	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 953	. . . . . 6 class y
8		cc0 5214	. . . . . . . 8 class 0
9	8	csn 2405	. . . . . . 7 class {0}
10	4, 9	cdif 2040	. . . . . 6 class (CC \ {0})
11	7, 10	wcel 956	. . . . 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 953	. . . . 5 class z
15		vw	. . . . . . . . . 10 set w
16	15	cv 953	. . . . . . . . 9 class w
17		cmul 5219	. . . . . . . . 9 class x.
18	7, 16, 17	co 3954	. . . . . . . 8 class (y x. w)
19	18, 3	wceq 954	. . . . . . 7 wff (y x. w) = x
20	19, 15, 4	crab 1645	. . . . . 6 class {w e. CC | (y x. w) = x}
21	20	cuni 2498	. . . . 5 class U.{w e. CC | (y x. w) = x}
22	14, 21	wceq 954	. . . 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 3955	. 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 954	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 5681

Copyright terms: Public domain