Metamath Proof Explorer

Theorem mapco2

Description: Post-composition (renaming indices) of a mapping viewed as a point. (Contributed by Stefan O'Rear, 5-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)

		Ref	Expression
	Hypothesis	mapco2.3	$⊢ E \in V$
	Assertion	mapco2	$⊢ (A \in (B^{C}) \land D : E ⟶ C) \to A \circ D \in (B^{E})$

Proof

Step	Hyp	Ref	Expression
1		mapco2.3	$⊢ E \in V$
2		mapco2g	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to A \circ D \in (B^{E})$
3	1 2	mp3an1	$⊢ (A \in (B^{C}) \land D : E ⟶ C) \to A \circ D \in (B^{E})$