pred_iii_restr

Theorem pred_iii_restr

Theorem. pred_iii_restr
A ⊆ B → (x ∈ B → y ∈ B → z ∈ B → P x y z) → (x ∈ A → y ∈ A → z ∈ A → P x y z)

Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ y ∈ A, hypo.
03. 3 ⊢ z ∈ A, hypo.
04. 4 ⊢ A ⊆ B, hypo.
05. 1, 4 ⊢ x ∈ B, incl_elim 4 1.
06. 2, 4 ⊢ y ∈ B, incl_elim 4 2.
07. 3, 4 ⊢ z ∈ B, incl_elim 4 3.
08. 8 ⊢ x ∈ B → y ∈ B → z ∈ B → P x y z, hypo.
09. 4, 8, 1 ⊢ y ∈ B → z ∈ B → P x y z, subj_elim 8 5.
10. 4, 8, 1, 2 ⊢ z ∈ B → P x y z, subj_elim 9 6.
11. 4, 8, 1, 2, 3 ⊢ P x y z, subj_elim 10 7.
12. 4, 8 ⊢ x ∈ A → y ∈ A → z ∈ A → P x y z, subj_intro_iii 11.
pred_iii_restr. ⊢ A ⊆ B → (x ∈ B → y ∈ B → z ∈ B → P x y z) →
  (x ∈ A → y ∈ A → z ∈ A → P x y z), subj_intro_ii 12.