This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )