uq_bounded

Theorem uq_bounded_elim

Theorem. uq_bounded_elim
(∀x. E x → P x) → E u → P u

Proof
01. 1 ⊢ ∀x. E x → P x, hypo.
02. 2 ⊢ E u, hypo.
03. 1 ⊢ E u → P u, uq_elim 1.
04. 1, 2 ⊢ P u, subj_elim 3 2.
uq_bounded_elim. ⊢ (∀x. E x → P x) → E u → P u, subj_intro_ii 4.