Definition df-rediv

Description: Define division between real numbers. This operator saves ax-mulcom over df-div in certain situations. (Contributed by SN, 25-Nov-2025)

	Ref	Expression
Assertion	df-rediv	$$⊢{/}_{ℝ}=\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		crediv	$$class{/}_{ℝ}$$
1		vx	$$setvarx$$
2		cr	$$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)$$