Theorem nat_rec_uniqueness

Proof
let rec f ↔ (∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n)).
01. 1 ⊢ app f 0 = x0 ∧ rec f, hypo.
02. 2 ⊢ app g 0 = x0 ∧ rec g, hypo.
03. 1 ⊢ app f 0 = x0, conj_eliml 1.
04. 2 ⊢ app g 0 = x0, conj_eliml 2.
05. 1, 2 ⊢ app f 0 = app g 0, eq_trans_rr 3 4.
06. 6 ⊢ n ∈ ℕ, hypo.
07. 7 ⊢ app f n = app g n, hypo.
08. 1 ⊢ rec f, conj_elimr 1.
09. 2 ⊢ rec g, conj_elimr 2.
10. 1, 6 ⊢ app f (n + 1) = φ n (app f n), uq_bounded_elim 8 6.
11. 2, 6 ⊢ app g (n + 1) = φ n (app g n), uq_bounded_elim 9 6.
12. 1, 6, 7 ⊢ app f (n + 1) = φ n (app g n),
  eq_subst 7 10, P t ↔ app f (n + 1) = φ n t.
13. 1, 2, 6, 7 ⊢ app f (n + 1) = app g (n + 1), eq_trans_rr 12 11.
14. 1, 2 ⊢ n ∈ ℕ → app f n = app g n →
  app f (n + 1) = app g (n + 1), subj_intro_ii 13.
15. 1, 2 ⊢ ∀n. n ∈ ℕ → app f n = app g n →
  app f (n + 1) = app g (n + 1), uq_intro 14.
16. 1, 2 ⊢ ∀n. n ∈ ℕ → app f n = app g n,
  nat_induction 5 15, P n ↔ app f n = app g n.
nat_rec_uniqueness. ⊢
  app f 0 = x0 ∧ (∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n)) →
  app g 0 = x0 ∧ (∀n. n ∈ ℕ → app g (n + 1) = φ n (app g n)) →
  ∀n. n ∈ ℕ → app f n = app g n, subj_intro_ii 16.

Dependencies
The given proof depends on seven axioms:
comp, eq_refl, eq_subst, ext, radd_closed, real_is_set, subset.