This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resmpt

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

		Ref	Expression
	Assertion	resmpt	$⊢ B \subseteq A \to {(x \in A ⟼ C) ↾}_{B} = (x \in B ⟼ C)$

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