Theorem rabs_symm

Proof
01. 1 ⊢ x ∈ ℝ, hypo.
02. ⊢ 0 ≤ x ∨ ¬0 ≤ x, lem.

03. 3 ⊢ 0 ≤ x, hypo.
04. 1, 3 ⊢ abs x = x, rabs_eql 1 3.
05. ⊢ 0 ∈ ℝ, calc.
06. 1, 3 ⊢ -x ≤ -0, rle_neg_swaps 5 1 3.
07. ⊢ -0 = 0, calc.
08. 1, 3 ⊢ -x ≤ 0, le_eq_trans 6 7.
09. 1 ⊢ -x ∈ ℝ, rneg_closed 1.
10. 1, 3 ⊢ abs (-x) = -(-x), rabs_non_positive 9 8.
11. 1 ⊢ -(-x) = x, rneg_involution 1.
12. 1, 3 ⊢ abs (-x) = x, eq_trans 10 11.
13. 1, 3 ⊢ abs (-x) = abs x, eq_trans_rr 12 4.

14. 14 ⊢ ¬0 ≤ x, hypo.
15. 1, 14 ⊢ abs x = -x, rabs_eqr 1 14.
16. 1, 14 ⊢ x ≤ 0, rle_neg 5 1 14.
17. 1, 14 ⊢ -0 ≤ -x, rle_neg_swaps 1 5 16.
18. ⊢ 0 = -0, calc.
19. 1, 14 ⊢ 0 ≤ -x, eq_le_trans 18 17.
20. 1, 14 ⊢ abs (-x) = -x, rabs_eql 9 19.
21. 1, 14 ⊢ abs (-x) = abs x, eq_trans_rr 20 15.

22. 1 ⊢ abs (-x) = abs x, disj_elim 2 13 21.
rabs_symm. ⊢ x ∈ ℝ → abs (-x) = abs x, subj_intro 22.

Dependencies
The given proof depends on 16 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_antisym, rle_compat_add, rle_refl, rle_total, rneg_closed.