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	|- ( ph -> A e. ( B ^m C ) )
	elmapssresd.2	|- ( ph -> D C_ C )
Assertion	elmapssresd	|- ( ph -> ( A |` D ) e. ( B ^m D ) )

Proof

Step	Hyp	Ref	Expression
1		elmapssresd.1	|- ( ph -> A e. ( B ^m C ) )
2		elmapssresd.2	|- ( ph -> D C_ C )
3		elmapssres	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( A |` D ) e. ( B ^m D ) )
4	1 2 3	syl2anc	|- ( ph -> ( A |` D ) e. ( B ^m D ) )