Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
|- ( A = B -> ( A e. _V <-> B e. _V ) ) |
2 |
|
preq2 |
|- ( A = B -> { C , A } = { C , B } ) |
3 |
2
|
preq2d |
|- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } ) |
4 |
3
|
eleq2d |
|- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) ) |
5 |
1 4
|
3anbi23d |
|- ( A = B -> ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) ) ) |
6 |
5
|
abbidv |
|- ( A = B -> { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } ) |
7 |
|
df-op |
|- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } |
8 |
|
df-op |
|- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } |
9 |
6 7 8
|
3eqtr4g |
|- ( A = B -> <. C , A >. = <. C , B >. ) |