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