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

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	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑_m 𝐶 ) )
	elmapssresd.2	⊢ ( 𝜑 → 𝐷 ⊆ 𝐶 )
Assertion	elmapssresd	⊢ ( 𝜑 → ( 𝐴 ↾ 𝐷 ) ∈ ( 𝐵 ↑_m 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		elmapssresd.1	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑_m 𝐶 ) )
2		elmapssresd.2	⊢ ( 𝜑 → 𝐷 ⊆ 𝐶 )
3		elmapssres	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑_m 𝐶 ) ∧ 𝐷 ⊆ 𝐶 ) → ( 𝐴 ↾ 𝐷 ) ∈ ( 𝐵 ↑_m 𝐷 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↾ 𝐷 ) ∈ ( 𝐵 ↑_m 𝐷 ) )