Let $(V,E)$ be a bipartite graph. I'm trying to capture this property and I've come up with two definitions and am surprised/confused that one uses a negation and the other doesn't - still I can't convert the one to the other.
So let $v,w$ be vertices in $V$ and let $X,Y$ denote subsets of $V$ with $X\cap Y=\emptyset$. I'd say bipartite means
"If the vertices $u$ and $v$ are connected, then one is in part $X$ and the other is in part $Y$."
$\exists X,Y.\ \forall u,v.\ [\ \{u,v\}\in E\implies (u\in X\land v\in Y)\lor (v\in X\land u\in Y)\ ]$
as well as
"If the vertices $u$ and $v$ are connected, then the don't belong to the same part."
$\exists X,Y.\ \forall u,v.\ [\ \{u,v\}\in E\implies \neg(u\in X\land v\in X)\land \neg(v\in Y\land u\in Y)\ ]$
I tried to use de Morgans law to change
$\{u,v\}\in E\implies (u\in X\land v\in Y)\lor (v\in X\land u\in Y)$
to
$\{u,v\}\in E\implies \neg(u\in X\land v\in X)\land \neg(v\in Y\land u\in Y)$
but can't get rid or produce the negations. Is there a set theoretical property I have to use, or must I maybe break out further of the $\implies$ conditional. Or did I just write down the axiomatization badly?