Metamath Proof Explorer

Theorem rediv11d

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

Ref Expression
Hypotheses rediv23d.a ⊢ φ → A ∈ ℝ
rediv23d.b ⊢ φ → B ∈ ℝ
rediv23d.c ⊢ φ → C ∈ ℝ
rediv23d.z ⊢ φ → C ≠ 0
Assertion rediv11d ⊢ φ → A / ℝ C = B / ℝ C ↔ A = B

Proof

Step Hyp Ref Expression
1 rediv23d.a ⊢ φ → A ∈ ℝ
2 rediv23d.b ⊢ φ → B ∈ ℝ
3 rediv23d.c ⊢ φ → C ∈ ℝ
4 rediv23d.z ⊢ φ → C ≠ 0
5 2 3 4 sn-redivcld ⊢ φ → B / ℝ C ∈ ℝ
6 1 5 3 4 redivmul2d ⊢ φ → A / ℝ C = B / ℝ C ↔ A = C ⁢ B / ℝ C
7 2 3 4 redivcan2d ⊢ φ → C ⁢ B / ℝ C = B
8 7 eqeq2d ⊢ φ → A = C ⁢ B / ℝ C ↔ A = B
9 6 8 bitrd ⊢ φ → A / ℝ C = B / ℝ C ↔ A = B