Theorem univ_closed_subset

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ y ⊆ x, hypo.
03. 3 ⊢ x ∈ U, hypo.
04. 1, 3 ⊢ power x ∈ U, univ_closed_power 1 3.
05. 1, 3 ⊢ power x ⊆ U, univ_trans 1 4.
06. 3 ⊢ set x, set_intro 3.
07. 2, 3 ⊢ set y, subset 2 6.
08. 2, 3 ⊢ y ∈ power x, power_intro 7 2.
09. 1, 2, 3 ⊢ y ∈ U, incl_elim 5 8.
univ_closed_subset. ⊢ univ U → y ⊆ x → x ∈ U → y ∈ U,
  subj_intro_iii 9.

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