Sobre la negación del bicondicional ya ha contestado Masacroso, pero este es un comentario muy interesante:
Sí, hay varias cosas que me chirrían en lo que expuse. Empezando por decir que una definición es una proposición. Lo cual es ¿mentira? porque sabemos que las definiciones no se demuestran ni se ponen contraejemplos.
Quizás al bicondicional habría que agregarle algunas hipótesis extra para que realmente se considere "una definición matemática", aunque ahora mismo no se me ocurre nada.
Pero esto lo pongo en duda al ver definiciones como las que plantea Masacroso o como muchísimas veces vimos que se define al límite puntual con un si y sólo si. Algo como:
\( \displaystyle\lim_{x\to a}f(x)=l\iff\ldots \)
¿Cuál sería entonces la negación de dicha definición de límite? 
Es que hay que entender bien el papel que juegan las definiciones en lógica formal. En principio, a un nivel totalmente formal, las únicas fórmulas válidas en matemáticas son las escritas en el lenguaje de la teoría de conjuntos. Es decir, las fórmulas únicamente pueden contener variables, conectores lógicos (esto incluye el signo de igualdad, \( = \)) y el símbolo \( \in \).
Cuando se introduce un nuevo símbolo en una definición, en realidad lo que se está haciendo es consensuar una abreviatura para una fórmula (o un término).
Por ejemplo, cuando introducimos el símbolo para la inclusión de conjuntos, \( \subset \), definimos \( A \subset B \) como que todo elemento de \( A \) es también un elemento de \( B \). Podríamos dar una definición de inclusión de conjuntos \( \subset \) en el estilo de la de límite así:
\( A \subset B \iff \forall x (x\in A \to x \in B) \)
Pero cuidado, porque esto
no es una fórmula válida. No puede serlo porque hemos dicho antes que las fórmulas o pueden contener símbolos que no sean conectores lógicos ni \( \in \), y esta contiene a \( \subset \).
Por eso, aunque a veces se escriban como "bicondicionales" hay que tener muy claro que las definiciones de ese tipo no son fórmulas lógicas, y que por tanto la flechita doble de ahí no es ningún conector lógico, es decir, no es ningún bicondicional.
Entonces, ¿qué significa exactamente hacer una definición y para qué sirve (a nivel lógico)?
Pues se hace simplemente para poder usar abreviaturas en las fórmulas lógicas, para hacerlas más legibles e inteligibles. Por ejemplo, para expresar que dos conjuntos \( A,B \) son iguales si cada uno es subconjunto del otro, escribiríamos:
\( \forall A \forall B (A \subset B \wedge B \subset A \to A=B) \).
Pero esto no es una fórmula válida en lógica de primer orden, estrictamente hablando, porque el símbolo \( \subset \) no pertenece al lenguaje.
La gracia de las definiciones es que como hemos definido \( A \subset B \) en términos de una fórmula que sí es válida, podemos interpretar la fórmula precedente como la fórmula en lógica de primer orden que resulta de sustituir cada aparición de \( A \subset B \) por su definición (el lado derecho), quedando así:
\( \forall A \forall B ((\forall x (x\in A \to x \in B) \wedge (\forall x (x \in B \to x \in A))\to A=B) \).
Esta sí que es una fórmula válida en el lenguaje de la teoría de conjuntos, pero para un humano es menos legible que la misma expresada con subconjuntos. Ahora imagina cómo sería una fórmula que involucrara conceptos como "función derivable" en términos únicamente de \( \in \). Sería una fórmula larguísima e incomprensible.
En resumen, las definiciones no forman parte de la lógica de primer orden y solamente representan abreviaturas de otras fórmulas. Por tanto el "bicondicional" en la definición que indicas no es ningún bicondicional porque esa fórmula no es una fórmula lógica. De la misma manera podríamos haber escrito algo como
\( A \subset B := \forall x (x\in A \to x \in B) \).
Espero que esto haya contribuido a aclarar las cosas y no a liarlas más.
