Metamath Proof Explorer

Theorem elmapssresd

Description: A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r with some reordering involving mapsspm . (Contributed by SN, 11-Mar-2025)

	Ref	Expression
Hypotheses	elmapssresd.1	$⊢ φ \to A \in (B^{C})$
	elmapssresd.2	$⊢ φ \to D \subseteq C$
Assertion	elmapssresd	$⊢ φ \to {A ↾}_{D} \in (B^{D})$

Proof

Step	Hyp	Ref	Expression
1		elmapssresd.1	$⊢ φ \to A \in (B^{C})$
2		elmapssresd.2	$⊢ φ \to D \subseteq C$
3		elmapssres	$⊢ (A \in (B^{C}) \land D \subseteq C) \to {A ↾}_{D} \in (B^{D})$
4	1 2 3	syl2anc	$⊢ φ \to {A ↾}_{D} \in (B^{D})$