Theorem Intersection_empty_set

Proof
01. 1 ⊢ x ∈ UnivCl, hypo.
02. 2 ⊢ A ∈ ∅, hypo.
03. 2 ⊢ x ∈ A, empty_efq 2.
04. ⊢ A ∈ ∅ → x ∈ A, subj_intro 3.
05. ⊢ ∀A. A ∈ ∅ → x ∈ A, uq_intro 4.
06. 1 ⊢ set x, set_intro 1.
08. 1 ⊢ x ∈ ⋂∅, Intersection_intro 6 5.
09. ⊢ x ∈ UnivCl → x ∈ ⋂∅, subj_intro 8.
10. ⊢ ∀x. x ∈ UnivCl → x ∈ ⋂∅, uq_intro 9.
11. ⊢ UnivCl ⊆ ⋂∅, incl_intro 10.
12. ⊢ ⋂∅ ⊆ UnivCl, UnivCl_is_greatest.
Intersection_empty_set. ⊢ ⋂∅ = UnivCl, incl_antisym 12 11.

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