Theorem compl_as_diff

Proof
01. 1 ⊢ x ∈ compl A, hypo.
02. 1 ⊢ set x, set_intro 1.
03. 1 ⊢ x ∈ UnivCl, UnivCl_intro 2.
04. 1 ⊢ ¬x ∈ A, compl_elim 1.
05. 1 ⊢ x ∈ UnivCl \ A, diff_intro 3 4.
06. ⊢ x ∈ compl A → x ∈ UnivCl \ A, subj_intro 5.
07. 7 ⊢ x ∈ UnivCl \ A, hypo.
08. 7 ⊢ set x, set_intro 7.
09. 7 ⊢ ¬x ∈ A, diff_elimr 7.
10. 7 ⊢ x ∈ compl A, compl_intro 8 9.
11. ⊢ x ∈ UnivCl \ A → x ∈ compl A, subj_intro 10.
12. ⊢ x ∈ compl A ↔ x ∈ UnivCl \ A, bij_intro 6 11.
13. ⊢ ∀x. x ∈ compl A ↔ x ∈ UnivCl \ A, uq_intro 12.
compl_as_diff. ⊢ compl A = UnivCl \ A, ext 13.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.