Theorem univ_closed_sep

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ A ∈ U, hypo.
03. ⊢ {x | x ∈ A ∧ P x} ⊆ A, sep_is_subclass.
04. 1, 2 ⊢ {x | x ∈ A ∧ P x} ∈ U, univ_closed_subset 1 3 2.
univ_closed_sep. ⊢ univ U → A ∈ U → {x | x ∈ A ∧ P x} ∈ U,
  subj_intro_ii 4.

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