resmpo

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013)

		Ref	Expression
	Assertion	resmpo	$⊢ (C \subseteq A \land D \subseteq B) \to {(x \in A, y \in B ⟼ E) ↾}_{(C \times D)} = (x \in C, y \in D ⟼ E)$

Step	Hyp	Ref	Expression
1		resoprab2	$⊢ (C \subseteq A \land D \subseteq B) \to {\{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = E)\} ↾}_{(C \times D)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land z = E)\}$
2		df-mpo	$⊢ (x \in A, y \in B ⟼ E) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = E)\}$
3	2	reseq1i	$⊢ {(x \in A, y \in B ⟼ E) ↾}_{(C \times D)} = {\{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = E)\} ↾}_{(C \times D)}$
4		df-mpo	$⊢ (x \in C, y \in D ⟼ E) = \{⟨⟨x, y⟩, z⟩ \| ((x \in C \land y \in D) \land z = E)\}$
5	1 3 4	3eqtr4g	$⊢ (C \subseteq A \land D \subseteq B) \to {(x \in A, y \in B ⟼ E) ↾}_{(C \times D)} = (x \in C, y \in D ⟼ E)$

Metamath Proof Explorer