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	|- /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crediv	|- /R
1		vx	|- x
2		cr	|- RR
3		vy	|- y
4		cc0	|- 0
5	4	csn	|- { 0 }
6	2 5	cdif	|- ( RR \ { 0 } )
7		vz	|- z
8	3	cv	|- y
9		cmul	|- x.
10	7	cv	|- z
11	8 10 9	co	|- ( y x. z )
12	1	cv	|- x
13	11 12	wceq	|- ( y x. z ) = x
14	13 7 2	crio	|- ( iota_ z e. RR ( y x. z ) = x )
15	1 3 2 6 14	cmpo	|- ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) )
16	0 15	wceq	|- /R = ( x e. RR , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR ( y x. z ) = x ) )