Step |
Hyp |
Ref |
Expression |
1 |
|
brcnvg |
|- ( ( A e. V /\ u e. _V ) -> ( A `' R u <-> u R A ) ) |
2 |
1
|
elvd |
|- ( A e. V -> ( A `' R u <-> u R A ) ) |
3 |
|
brcnvg |
|- ( ( B e. W /\ u e. _V ) -> ( B `' R u <-> u R B ) ) |
4 |
3
|
elvd |
|- ( B e. W -> ( B `' R u <-> u R B ) ) |
5 |
2 4
|
bi2anan9 |
|- ( ( A e. V /\ B e. W ) -> ( ( A `' R u /\ B `' R u ) <-> ( u R A /\ u R B ) ) ) |
6 |
5
|
exbidv |
|- ( ( A e. V /\ B e. W ) -> ( E. u ( A `' R u /\ B `' R u ) <-> E. u ( u R A /\ u R B ) ) ) |
7 |
|
ecinn0 |
|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] `' R i^i [ B ] `' R ) =/= (/) <-> E. u ( A `' R u /\ B `' R u ) ) ) |
8 |
|
brcoss |
|- ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( u R A /\ u R B ) ) ) |
9 |
6 7 8
|
3bitr4rd |
|- ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> ( [ A ] `' R i^i [ B ] `' R ) =/= (/) ) ) |