Theorem. pred_restr
A ⊆ B → (x ∈ B → P x) →
(x ∈ A → P x)
Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ A ⊆ B, hypo.
03. 1, 2 ⊢ x ∈ B, incl_elim 2 1.
04. 4 ⊢ x ∈ B → P x, hypo.
05. 2, 4, 1 ⊢ P x, subj_elim 4 3.
pred_restr. ⊢ A ⊆ B → (x ∈ B → P x) →
(x ∈ A → P x), subj_intro_iii 5.