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	Could not format assertion : No typesetting found for |- /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crediv	Could not format /R : No typesetting found for class /R with typecode 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	Could not format /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) ) : No typesetting found for wff /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) ) with typecode wff