Metamath Proof Explorer

Theorem resoprab2

Description: Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion resoprab2 ⊢ C ⊆ A ∧ D ⊆ B → x y z | x ∈ A ∧ y ∈ B ∧ φ ↾ C × D = x y z | x ∈ C ∧ y ∈ D ∧ φ

Proof

Step Hyp Ref Expression
1 resoprab ⊢ x y z | x ∈ A ∧ y ∈ B ∧ φ ↾ C × D = x y z | x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ∧ φ
2 anass ⊢ x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ∧ φ ↔ x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ∧ φ
3 an4 ⊢ x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ↔ x ∈ C ∧ x ∈ A ∧ y ∈ D ∧ y ∈ B
4 ssel ⊢ C ⊆ A → x ∈ C → x ∈ A
5 4 pm4.71d ⊢ C ⊆ A → x ∈ C ↔ x ∈ C ∧ x ∈ A
6 5 bicomd ⊢ C ⊆ A → x ∈ C ∧ x ∈ A ↔ x ∈ C
7 ssel ⊢ D ⊆ B → y ∈ D → y ∈ B
8 7 pm4.71d ⊢ D ⊆ B → y ∈ D ↔ y ∈ D ∧ y ∈ B
9 8 bicomd ⊢ D ⊆ B → y ∈ D ∧ y ∈ B ↔ y ∈ D
10 6 9 bi2anan9 ⊢ C ⊆ A ∧ D ⊆ B → x ∈ C ∧ x ∈ A ∧ y ∈ D ∧ y ∈ B ↔ x ∈ C ∧ y ∈ D
11 3 10 syl5bb ⊢ C ⊆ A ∧ D ⊆ B → x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ↔ x ∈ C ∧ y ∈ D
12 11 anbi1d ⊢ C ⊆ A ∧ D ⊆ B → x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ∧ φ ↔ x ∈ C ∧ y ∈ D ∧ φ
13 2 12 bitr3id ⊢ C ⊆ A ∧ D ⊆ B → x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ∧ φ ↔ x ∈ C ∧ y ∈ D ∧ φ
14 13 oprabbidv ⊢ C ⊆ A ∧ D ⊆ B → x y z | x ∈ C ∧ y ∈ D ∧ x ∈ A ∧ y ∈ B ∧ φ = x y z | x ∈ C ∧ y ∈ D ∧ φ
15 1 14 syl5eq ⊢ C ⊆ A ∧ D ⊆ B → x y z | x ∈ A ∧ y ∈ B ∧ φ ↾ C × D = x y z | x ∈ C ∧ y ∈ D ∧ φ