Step |
Hyp |
Ref |
Expression |
1 |
|
relcnv |
|- Rel `' ( A o. `' B ) |
2 |
|
relco |
|- Rel ( B o. `' A ) |
3 |
|
vex |
|- y e. _V |
4 |
|
vex |
|- z e. _V |
5 |
3 4
|
brcnv |
|- ( y `' B z <-> z B y ) |
6 |
|
vex |
|- x e. _V |
7 |
6 4
|
brcnv |
|- ( x `' A z <-> z A x ) |
8 |
7
|
bicomi |
|- ( z A x <-> x `' A z ) |
9 |
5 8
|
anbi12ci |
|- ( ( y `' B z /\ z A x ) <-> ( x `' A z /\ z B y ) ) |
10 |
9
|
exbii |
|- ( E. z ( y `' B z /\ z A x ) <-> E. z ( x `' A z /\ z B y ) ) |
11 |
6 3
|
opelcnv |
|- ( <. x , y >. e. `' ( A o. `' B ) <-> <. y , x >. e. ( A o. `' B ) ) |
12 |
3 6
|
opelco |
|- ( <. y , x >. e. ( A o. `' B ) <-> E. z ( y `' B z /\ z A x ) ) |
13 |
11 12
|
bitri |
|- ( <. x , y >. e. `' ( A o. `' B ) <-> E. z ( y `' B z /\ z A x ) ) |
14 |
6 3
|
opelco |
|- ( <. x , y >. e. ( B o. `' A ) <-> E. z ( x `' A z /\ z B y ) ) |
15 |
10 13 14
|
3bitr4i |
|- ( <. x , y >. e. `' ( A o. `' B ) <-> <. x , y >. e. ( B o. `' A ) ) |
16 |
1 2 15
|
eqrelriiv |
|- `' ( A o. `' B ) = ( B o. `' A ) |