\begin{abbreviation}\label{empty}
    $x$ is empty iff there exists no $y$ such that $y\in x$.
\end{abbreviation}

\begin{proposition}\label{dummy_abbr_test_adj}
   If $x$ is empty, then $x$ is empty.
\end{proposition}


% Dummy abbreviation to test noun abbreviations.
\begin{abbreviation}\label{function}
    $x$ is a function iff $x = x$.
\end{abbreviation}

\begin{proposition}\label{dummy_abbr_test_noun}
    $x$ is a function.
 \end{proposition}


% Dummy abbreviation to test verb abbreviations.
\begin{abbreviation}\label{converges}
    $x$ converges to $y$ iff $x = y$.
\end{abbreviation}

\begin{proposition}\label{dummy_abbr_test_verb}
    If $x$ converges to $y$, then $x = y$.
 \end{proposition}


% Test of built-in \notin abbreviation. The two variants should produce the same TPTP atoms.
\begin{proposition}\label{abbr_test_notin}
   If $x\notin y$, then $x\not\in y$.
\end{proposition}


% Test of built-in "element of" abbreviation. The two variants should produce the same TPTP atoms.
\begin{proposition}\label{abbr_test_elementof_is_in}
    If $x$ is an element of $y$, then $x\in y$.
\end{proposition}


% Test of built-in "equals" abbreviation. The two variants should produce the same TPTP atoms.
\begin{proposition}\label{abbr_test_equals_is_eq}
    If $x$ equals $y$, then $x = y$.
\end{proposition}