Metamath Proof Explorer

Theorem resoprab2

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

		Ref	Expression
	Assertion	resoprab2	$⊢ (C \subseteq A \land D \subseteq B) \to {\{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} ↾}_{(C \times D)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land φ)\}$

Proof

Step	Hyp	Ref	Expression
1		resoprab	$⊢ {\{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} ↾}_{(C \times D)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land ((x \in A \land y \in B) \land φ))\}$
2		anass	$⊢ (((x \in C \land y \in D) \land (x \in A \land y \in B)) \land φ) \leftrightarrow ((x \in C \land y \in D) \land ((x \in A \land y \in B) \land φ))$
3		an4	$⊢ ((x \in C \land y \in D) \land (x \in A \land y \in B)) \leftrightarrow ((x \in C \land x \in A) \land (y \in D \land y \in B))$
4		ssel	$⊢ C \subseteq A \to (x \in C \to x \in A)$
5	4	pm4.71d	$⊢ C \subseteq A \to (x \in C \leftrightarrow (x \in C \land x \in A))$
6	5	bicomd	$⊢ C \subseteq A \to ((x \in C \land x \in A) \leftrightarrow x \in C)$
7		ssel	$⊢ D \subseteq B \to (y \in D \to y \in B)$
8	7	pm4.71d	$⊢ D \subseteq B \to (y \in D \leftrightarrow (y \in D \land y \in B))$
9	8	bicomd	$⊢ D \subseteq B \to ((y \in D \land y \in B) \leftrightarrow y \in D)$
10	6 9	bi2anan9	$⊢ (C \subseteq A \land D \subseteq B) \to (((x \in C \land x \in A) \land (y \in D \land y \in B)) \leftrightarrow (x \in C \land y \in D))$
11	3 10	bitrid	$⊢ (C \subseteq A \land D \subseteq B) \to (((x \in C \land y \in D) \land (x \in A \land y \in B)) \leftrightarrow (x \in C \land y \in D))$
12	11	anbi1d	$⊢ (C \subseteq A \land D \subseteq B) \to ((((x \in C \land y \in D) \land (x \in A \land y \in B)) \land φ) \leftrightarrow ((x \in C \land y \in D) \land φ))$
13	2 12	bitr3id	$⊢ (C \subseteq A \land D \subseteq B) \to (((x \in C \land y \in D) \land ((x \in A \land y \in B) \land φ)) \leftrightarrow ((x \in C \land y \in D) \land φ))$
14	13	oprabbidv	$⊢ (C \subseteq A \land D \subseteq B) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land ((x \in A \land y \in B) \land φ))\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land φ)\}$
15	1 14	eqtrid	$⊢ (C \subseteq A \land D \subseteq B) \to {\{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} ↾}_{(C \times D)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land φ)\}$