Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 1 ⊢ a + 0 = a, radd_neutr 1. 03. ⊢ 0 = -0, calc. 04. ⊢ a - 0 = a + -0, rsub_eq. 05. 1 ⊢ a + -0 = a, eq_subst 3 2, P t ↔ a + t = a. 06. 1 ⊢ a - 0 = a, eq_trans 4 5. rsub_zero. ⊢ a ∈ ℝ → a - 0 = a, subj_intro 6.
Dependencies
The given proof depends on three axioms:
eq_refl, eq_subst, radd_neutr.