Step |
Hyp |
Ref |
Expression |
1 |
|
cnvsn.1 |
|- A e. _V |
2 |
|
cnvsn.2 |
|- B e. _V |
3 |
1 2
|
cnvsn |
|- `' { <. A , B >. } = { <. B , A >. } |
4 |
3
|
inteqi |
|- |^| `' { <. A , B >. } = |^| { <. B , A >. } |
5 |
|
opex |
|- <. B , A >. e. _V |
6 |
5
|
intsn |
|- |^| { <. B , A >. } = <. B , A >. |
7 |
4 6
|
eqtri |
|- |^| `' { <. A , B >. } = <. B , A >. |
8 |
7
|
inteqi |
|- |^| |^| `' { <. A , B >. } = |^| <. B , A >. |
9 |
8
|
inteqi |
|- |^| |^| |^| `' { <. A , B >. } = |^| |^| <. B , A >. |
10 |
2 1
|
op1stb |
|- |^| |^| <. B , A >. = B |
11 |
9 10
|
eqtri |
|- |^| |^| |^| `' { <. A , B >. } = B |