Theorem rediv11d

Description: One-to-one relationship for division. (Contributed by SN, 9-Apr-2026)

	Ref	Expression
Hypotheses	rediv23d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	rediv23d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	rediv23d.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	rediv23d.z	⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion	rediv11d	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = ( 𝐵 /ℝ 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rediv23d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		rediv23d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		rediv23d.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		rediv23d.z	⊢ ( 𝜑 → 𝐶 ≠ 0 )
5	2 3 4	sn-redivcld	⊢ ( 𝜑 → ( 𝐵 /ℝ 𝐶 ) ∈ ℝ )
6	1 5 3 4	redivmul2d	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = ( 𝐵 /ℝ 𝐶 ) ↔ 𝐴 = ( 𝐶 · ( 𝐵 /ℝ 𝐶 ) ) ) )
7	2 3 4	redivcan2d	⊢ ( 𝜑 → ( 𝐶 · ( 𝐵 /ℝ 𝐶 ) ) = 𝐵 )
8	7	eqeq2d	⊢ ( 𝜑 → ( 𝐴 = ( 𝐶 · ( 𝐵 /ℝ 𝐶 ) ) ↔ 𝐴 = 𝐵 ) )
9	6 8	bitrd	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = ( 𝐵 /ℝ 𝐶 ) ↔ 𝐴 = 𝐵 ) )