Theorem csbmpt2

Description: Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019)

	Ref	Expression
Assertion	csbmpt2	$$⊢A\in V\to ⦋A/x⦌\left(y\in Y⟼Z\right)=\left(y\in Y⟼⦋A/x⦌Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbmpt12	$$⊢A\in V\to ⦋A/x⦌\left(y\in Y⟼Z\right)=\left(y\in ⦋A/x⦌Y⟼⦋A/x⦌Z\right)$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌Y=Y$$
3	2	mpteq1d	$$⊢A\in V\to \left(y\in ⦋A/x⦌Y⟼⦋A/x⦌Z\right)=\left(y\in Y⟼⦋A/x⦌Z\right)$$
4	1 3	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left(y\in Y⟼Z\right)=\left(y\in Y⟼⦋A/x⦌Z\right)$$