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	⊢ /ℝ = ( 𝑥 ∈ ℝ , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℝ ( 𝑦 · 𝑧 ) = 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crediv	⊢ /ℝ
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		vy	⊢ 𝑦
4		cc0	⊢ 0
5	4	csn	⊢ { 0 }
6	2 5	cdif	⊢ ( ℝ ∖ { 0 } )
7		vz	⊢ 𝑧
8	3	cv	⊢ 𝑦
9		cmul	⊢ ·
10	7	cv	⊢ 𝑧
11	8 10 9	co	⊢ ( 𝑦 · 𝑧 )
12	1	cv	⊢ 𝑥
13	11 12	wceq	⊢ ( 𝑦 · 𝑧 ) = 𝑥
14	13 7 2	crio	⊢ ( ℩ 𝑧 ∈ ℝ ( 𝑦 · 𝑧 ) = 𝑥 )
15	1 3 2 6 14	cmpo	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℝ ( 𝑦 · 𝑧 ) = 𝑥 ) )
16	0 15	wceq	⊢ /ℝ = ( 𝑥 ∈ ℝ , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℝ ( 𝑦 · 𝑧 ) = 𝑥 ) )