pred_ii_restr

Theorem pred_ii_restr

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

Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ y ∈ A, hypo.
03. 3 ⊢ A ⊆ B, hypo.
04. 1, 3 ⊢ x ∈ B, incl_elim 3 1.
05. 2, 3 ⊢ y ∈ B, incl_elim 3 2.
06. 6 ⊢ x ∈ B → y ∈ B → P x y, hypo.
07. 3, 6, 1 ⊢ y ∈ B → P x y, subj_elim 6 4.
08. 3, 6, 1, 2 ⊢ P x y, subj_elim 7 5.
pred_ii_restr. ⊢ A ⊆ B → (x ∈ B → y ∈ B → P x y) →
  (x ∈ A → y ∈ A → P x y), subj_intro_iv 8.