Step |
Hyp |
Ref |
Expression |
1 |
|
df-ne |
|- ( <. A , B >. =/= <. C , D >. <-> -. <. A , B >. = <. C , D >. ) |
2 |
|
opthg |
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) ) |
3 |
2
|
notbid |
|- ( ( A e. V /\ B e. W ) -> ( -. <. A , B >. = <. C , D >. <-> -. ( A = C /\ B = D ) ) ) |
4 |
|
ianor |
|- ( -. ( A = C /\ B = D ) <-> ( -. A = C \/ -. B = D ) ) |
5 |
|
df-ne |
|- ( A =/= C <-> -. A = C ) |
6 |
|
df-ne |
|- ( B =/= D <-> -. B = D ) |
7 |
5 6
|
orbi12i |
|- ( ( A =/= C \/ B =/= D ) <-> ( -. A = C \/ -. B = D ) ) |
8 |
4 7
|
bitr4i |
|- ( -. ( A = C /\ B = D ) <-> ( A =/= C \/ B =/= D ) ) |
9 |
3 8
|
bitrdi |
|- ( ( A e. V /\ B e. W ) -> ( -. <. A , B >. = <. C , D >. <-> ( A =/= C \/ B =/= D ) ) ) |
10 |
1 9
|
syl5bb |
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. =/= <. C , D >. <-> ( A =/= C \/ B =/= D ) ) ) |