Theorem separation_is_unique

If there exists a separation set, i.e., the axiom of separation holds for A with respect to P, this set exists uniquely. Since the proof depends solely on the extensionality axiom, this uniqueness holds in any fragmental system of set theory to which the separation axiom is to be added.

Proof
let S B ↔ (∀x. x ∈ B ↔ x ∈ A ∧ P x).
01. 1 ⊢ ∃B. S B, hypo.
02. 2 ⊢ S B1, hypo.
03. 3 ⊢ S B2, hypo.
04. 2 ⊢ x ∈ B1 ↔ x ∈ A ∧ P x, uq_elim 2.
05. 3 ⊢ x ∈ B2 ↔ x ∈ A ∧ P x, uq_elim 3.
06. 2, 3 ⊢ x ∈ B1 ↔ x ∈ B2, equi_trans_rr 4 5.
07. 2, 3 ⊢ ∀x. x ∈ B1 ↔ x ∈ B2, uq_intro 6.
08. 2, 3 ⊢ B1 = B2, ext 7.
09. ⊢ S B1 → S B2 → B1 = B2, subj_intro_ii 8.
10. ⊢ ∀B2. S B1 → S B2 → B1 = B2, uq_intro 9.
11. ⊢ ∀B1. ∀B2. S B1 → S B2 → B1 = B2, uq_intro 10.
12. 1 ⊢ ∃C. ∀B. C = B ↔ S B, ex_uniq_intro 1 11.
separation_is_unique. ⊢ (∃B. ∀x. x ∈ B ↔ x ∈ A ∧ P x) →
  (∃C. ∀B. C = B ↔ ∀x. x ∈ B ↔ x ∈ A ∧ P x), subj_intro 12.

Dependencies
The given proof depends on two axioms:
eq_subst, ext.