# Metamath Proof Explorer

## 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 ℂ|{y}{z}={x}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cdiv ${class}÷$
1 vx ${setvar}{x}$
2 cc ${class}ℂ$
3 vy ${setvar}{y}$
4 cc0 ${class}0$
5 4 csn ${class}\left\{0\right\}$
6 2 5 cdif ${class}\left(ℂ\setminus \left\{0\right\}\right)$
7 vz ${setvar}{z}$
8 3 cv ${setvar}{y}$
9 cmul ${class}×$
10 7 cv ${setvar}{z}$
11 8 10 9 co ${class}{y}{z}$
12 1 cv ${setvar}{x}$
13 11 12 wceq ${wff}{y}{z}={x}$
14 13 7 2 crio ${class}\left(\iota {z}\in ℂ|{y}{z}={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 ℂ|{y}{z}={x}\right)\right)$
16 0 15 wceq ${wff}÷=\left({x}\in ℂ,{y}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota {z}\in ℂ|{y}{z}={x}\right)\right)$