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

Metamath Proof Explorer

Theorem resmptd

Description: Restriction of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	resmptd.b	$⊢ φ \to B \subseteq A$
	Assertion	resmptd	$⊢ φ \to {(x \in A ⟼ C) ↾}_{B} = (x \in B ⟼ C)$

Step	Hyp	Ref	Expression
1		resmptd.b	$⊢ φ \to B \subseteq A$
2		resmpt	$⊢ B \subseteq A \to {(x \in A ⟼ C) ↾}_{B} = (x \in B ⟼ C)$
3	1 2	syl	$⊢ φ \to {(x \in A ⟼ C) ↾}_{B} = (x \in B ⟼ C)$