Definition df-div

Description: Define division. Theorem divmuli relates it to multiplication, and divcli and redivcli prove its closure laws. (Contributed by NM, 2-Feb-1995) Use divval instead. (Revised by Mario Carneiro, 1-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	df-div	$$⊢÷=\left(x\in ℂ,y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota z\in ℂ|yz=x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdiv	$$class÷$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vy	$$setvary$$
4		cc0	$$class0$$
5	4	csn	$$class\left\{0\right\}$$
6	2 5	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
7		vz	$$setvarz$$
8	3	cv	$$setvary$$
9		cmul	$$class\times$$
10	7	cv	$$setvarz$$
11	8 10 9	co	$$classyz$$
12	1	cv	$$setvarx$$
13	11 12	wceq	$$wffyz=x$$
14	13 7 2	crio	$$class\left(\iota z\in ℂ|yz=x\right)$$
15	1 3 2 6 14	cmpo	$$class\left(x\in ℂ,y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota z\in ℂ|yz=x\right)\right)$$
16	0 15	wceq	$$wff÷=\left(x\in ℂ,y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota z\in ℂ|yz=x\right)\right)$$