Step |
Hyp |
Ref |
Expression |
1 |
|
br1cossxrnres |
|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _S |` A ) ) <. D , E >. <-> E. u e. A ( ( u `' _S C /\ u R B ) /\ ( u `' _S E /\ u R D ) ) ) ) |
2 |
|
brcnvssr |
|- ( u e. _V -> ( u `' _S C <-> C C_ u ) ) |
3 |
2
|
elv |
|- ( u `' _S C <-> C C_ u ) |
4 |
3
|
anbi1i |
|- ( ( u `' _S C /\ u R B ) <-> ( C C_ u /\ u R B ) ) |
5 |
|
brcnvssr |
|- ( u e. _V -> ( u `' _S E <-> E C_ u ) ) |
6 |
5
|
elv |
|- ( u `' _S E <-> E C_ u ) |
7 |
6
|
anbi1i |
|- ( ( u `' _S E /\ u R D ) <-> ( E C_ u /\ u R D ) ) |
8 |
4 7
|
anbi12i |
|- ( ( ( u `' _S C /\ u R B ) /\ ( u `' _S E /\ u R D ) ) <-> ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) ) |
9 |
8
|
rexbii |
|- ( E. u e. A ( ( u `' _S C /\ u R B ) /\ ( u `' _S E /\ u R D ) ) <-> E. u e. A ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) ) |
10 |
1 9
|
bitrdi |
|- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( `' _S |` A ) ) <. D , E >. <-> E. u e. A ( ( C C_ u /\ u R B ) /\ ( E C_ u /\ u R D ) ) ) ) |