Theorem csbmpt12

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

	Ref	Expression
Assertion	csbmpt12	|- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) )

Proof

Step	Hyp	Ref	Expression
1		csbopab	|- [_ A / x ]_ { <. y , z >. | ( y e. Y /\ z = Z ) } = { <. y , z >. | [. A / x ]. ( y e. Y /\ z = Z ) }
2		sbcan	|- ( [. A / x ]. ( y e. Y /\ z = Z ) <-> ( [. A / x ]. y e. Y /\ [. A / x ]. z = Z ) )
3		sbcel12	|- ( [. A / x ]. y e. Y <-> [_ A / x ]_ y e. [_ A / x ]_ Y )
4		csbconstg	|- ( A e. V -> [_ A / x ]_ y = y )
5	4	eleq1d	|- ( A e. V -> ( [_ A / x ]_ y e. [_ A / x ]_ Y <-> y e. [_ A / x ]_ Y ) )
6	3 5	bitrid	|- ( A e. V -> ( [. A / x ]. y e. Y <-> y e. [_ A / x ]_ Y ) )
7		sbceq2g	|- ( A e. V -> ( [. A / x ]. z = Z <-> z = [_ A / x ]_ Z ) )
8	6 7	anbi12d	|- ( A e. V -> ( ( [. A / x ]. y e. Y /\ [. A / x ]. z = Z ) <-> ( y e. [_ A / x ]_ Y /\ z = [_ A / x ]_ Z ) ) )
9	2 8	bitrid	|- ( A e. V -> ( [. A / x ]. ( y e. Y /\ z = Z ) <-> ( y e. [_ A / x ]_ Y /\ z = [_ A / x ]_ Z ) ) )
10	9	opabbidv	|- ( A e. V -> { <. y , z >. | [. A / x ]. ( y e. Y /\ z = Z ) } = { <. y , z >. | ( y e. [_ A / x ]_ Y /\ z = [_ A / x ]_ Z ) } )
11	1 10	eqtrid	|- ( A e. V -> [_ A / x ]_ { <. y , z >. | ( y e. Y /\ z = Z ) } = { <. y , z >. | ( y e. [_ A / x ]_ Y /\ z = [_ A / x ]_ Z ) } )
12		df-mpt	|- ( y e. Y |-> Z ) = { <. y , z >. | ( y e. Y /\ z = Z ) }
13	12	csbeq2i	|- [_ A / x ]_ ( y e. Y |-> Z ) = [_ A / x ]_ { <. y , z >. | ( y e. Y /\ z = Z ) }
14		df-mpt	|- ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) = { <. y , z >. | ( y e. [_ A / x ]_ Y /\ z = [_ A / x ]_ Z ) }
15	11 13 14	3eqtr4g	|- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) )