Theorem univ_closed_power

Theorem. univ_closed_power
univ U → x ∈ U → power x ∈ U
Proof
01. 1 ⊢ univ U, hypo.
02. 1 ⊢ (∀x. x ∈ U → power x ∈ U), lsubj_conj_elimlr univ_equi 1.
03. 1 ⊢ x ∈ U → power x ∈ U, uq_elim 2.
univ_closed_power. ⊢ univ U → x ∈ U → power x ∈ U, subj_intro 3.