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 e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. Y |-> [_ A / x ]_ Z ) )

Proof

Step	Hyp	Ref	Expression
1		csbmpt12	|- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) )
2		csbconstg	|- ( A e. V -> [_ A / x ]_ Y = Y )
3	2	mpteq1d	|- ( A e. V -> ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) = ( y e. Y |-> [_ A / x ]_ Z ) )
4	1 3	eqtrd	|- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. Y |-> [_ A / x ]_ Z ) )