Metamath Proof Explorer

Theorem csbmpo123

Description: Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 csboprabg 
 |-  ( A e. V -> [_ A / x ]_ { <. <. y , z >. , d >. | ( ( y e. Y /\ z e. Z ) /\ d = D ) } = { <. <. y , z >. , d >. | [. A / x ]. ( ( y e. Y /\ z e. Z ) /\ d = D ) } )
2 sbcan 
 |-  ( [. A / x ]. ( ( y e. Y /\ z e. Z ) /\ d = D ) <-> ( [. A / x ]. ( y e. Y /\ z e. Z ) /\ [. A / x ]. d = D ) )
3 sbcan 
 |-  ( [. A / x ]. ( y e. Y /\ z e. Z ) <-> ( [. A / x ]. y e. Y /\ [. A / x ]. z e. Z ) )
4 sbcel12 
 |-  ( [. A / x ]. y e. Y <-> [_ A / x ]_ y e. [_ A / x ]_ Y )
5 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ y = y )
6 5 eleq1d 
 |-  ( A e. V -> ( [_ A / x ]_ y e. [_ A / x ]_ Y <-> y e. [_ A / x ]_ Y ) )
7 4 6 bitrid 
 |-  ( A e. V -> ( [. A / x ]. y e. Y <-> y e. [_ A / x ]_ Y ) )
8 sbcel12 
 |-  ( [. A / x ]. z e. Z <-> [_ A / x ]_ z e. [_ A / x ]_ Z )
9 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ z = z )
10 9 eleq1d 
 |-  ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ Z <-> z e. [_ A / x ]_ Z ) )
11 8 10 bitrid 
 |-  ( A e. V -> ( [. A / x ]. z e. Z <-> z e. [_ A / x ]_ Z ) )
12 7 11 anbi12d 
 |-  ( A e. V -> ( ( [. A / x ]. y e. Y /\ [. A / x ]. z e. Z ) <-> ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) ) )
13 3 12 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( y e. Y /\ z e. Z ) <-> ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) ) )
14 sbceq2g 
 |-  ( A e. V -> ( [. A / x ]. d = D <-> d = [_ A / x ]_ D ) )
15 13 14 anbi12d 
 |-  ( A e. V -> ( ( [. A / x ]. ( y e. Y /\ z e. Z ) /\ [. A / x ]. d = D ) <-> ( ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) /\ d = [_ A / x ]_ D ) ) )
16 2 15 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( ( y e. Y /\ z e. Z ) /\ d = D ) <-> ( ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) /\ d = [_ A / x ]_ D ) ) )
17 16 oprabbidv 
 |-  ( A e. V -> { <. <. y , z >. , d >. | [. A / x ]. ( ( y e. Y /\ z e. Z ) /\ d = D ) } = { <. <. y , z >. , d >. | ( ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) /\ d = [_ A / x ]_ D ) } )
18 1 17 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ { <. <. y , z >. , d >. | ( ( y e. Y /\ z e. Z ) /\ d = D ) } = { <. <. y , z >. , d >. | ( ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) /\ d = [_ A / x ]_ D ) } )
19 df-mpo 
 |-  ( y e. Y , z e. Z |-> D ) = { <. <. y , z >. , d >. | ( ( y e. Y /\ z e. Z ) /\ d = D ) }
20 19 csbeq2i 
 |-  [_ A / x ]_ ( y e. Y , z e. Z |-> D ) = [_ A / x ]_ { <. <. y , z >. , d >. | ( ( y e. Y /\ z e. Z ) /\ d = D ) }
21 df-mpo 
 |-  ( y e. [_ A / x ]_ Y , z e. [_ A / x ]_ Z |-> [_ A / x ]_ D ) = { <. <. y , z >. , d >. | ( ( y e. [_ A / x ]_ Y /\ z e. [_ A / x ]_ Z ) /\ d = [_ A / x ]_ D ) }
22 18 20 21 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ ( y e. Y , z e. Z |-> D ) = ( y e. [_ A / x ]_ Y , z e. [_ A / x ]_ Z |-> [_ A / x ]_ D ) )