Definition df-xdiv

Description: Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	df-xdiv	$$⊢{÷}_{𝑒}=\left(x\in {ℝ}^{*},y\in \left(ℝ\setminus \left\{0\right\}\right)⟼\left(\iota z\in {ℝ}^{*}|y{\cdot }_{𝑒}z=x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxdiv	$$class{÷}_{𝑒}$$
1		vx	$$setvarx$$
2		cxr	$$class{ℝ}^{*}$$
3		vy	$$setvary$$
4		cr	$$classℝ$$
5		cc0	$$class0$$
6	5	csn	$$class\left\{0\right\}$$
7	4 6	cdif	$$class\left(ℝ\setminus \left\{0\right\}\right)$$
8		vz	$$setvarz$$
9	3	cv	$$setvary$$
10		cxmu	$$class{\cdot }_{𝑒}$$
11	8	cv	$$setvarz$$
12	9 11 10	co	$$class\left(y{\cdot }_{𝑒}z\right)$$
13	1	cv	$$setvarx$$
14	12 13	wceq	$$wffy{\cdot }_{𝑒}z=x$$
15	14 8 2	crio	$$class\left(\iota z\in {ℝ}^{*}|y{\cdot }_{𝑒}z=x\right)$$
16	1 3 2 7 15	cmpo	$$class\left(x\in {ℝ}^{*},y\in \left(ℝ\setminus \left\{0\right\}\right)⟼\left(\iota z\in {ℝ}^{*}|y{\cdot }_{𝑒}z=x\right)\right)$$
17	0 16	wceq	$$wff{÷}_{𝑒}=\left(x\in {ℝ}^{*},y\in \left(ℝ\setminus \left\{0\right\}\right)⟼\left(\iota z\in {ℝ}^{*}|y{\cdot }_{𝑒}z=x\right)\right)$$