Prove that $(S \cap T = \varnothing) \land (S \cup T = T) \rightarrow S = \varnothing$. Logically, the following proposition makes sense:
$(S \cap T = \varnothing) \land (S \cup T = T) \rightarrow S = \varnothing$
Or, in english, if sets $S$ and $T$ share no elements, and the union of the sets is equal to one of the sets, then the other set must be empty.
However, what I'm struggling with is how to translate this english into mathematical symbols.
Would anyone know how to solve this with mathematical symbols?
 A: $$ (S \cap T = \varnothing)\tag{1}$$
$$(S \cup T = T) \tag{2}$$
Now:
Starting with $(2)$
$$S \cup T = T \implies S \subseteq T \implies S \cap T = S$$
Since we have $(1): S\cap T = \varnothing$, then $$S\cap T = S = \varnothing$$
A: Here is an element-level calculational solution, which only uses the set theory definitions and predicate logic.
Expanding the definitions in the first part, and doing some simplification, results in
\begin{align}
& S \cap T = \varnothing \\
\equiv & \;\;\;\;\;\text{"extensionality; definitions of $\;\varnothing,\cap\;$"} \\
& \langle \forall x :: \lnot(x \in S \land x \in T) \rangle \\
\equiv & \;\;\;\;\;\text{"logic: DeMorgan"} \\
& \langle \forall x :: x \not\in S \lor x \not\in T \rangle \\
\end{align}
For the second part, we get
\begin{align}
& S \cup T = T \\
\equiv & \;\;\;\;\;\text{"extensionality; definition of $\;\cup\;$"} \\
& \langle \forall x :: x \in S \lor x \in T \equiv x \in T \rangle \\
\equiv & \;\;\;\;\;\text{"logic: $\;p \lor q \equiv q\;$ is one way to write $\;p \Rightarrow q\;$"} \\
& \langle \forall x :: x \in S \Rightarrow x \in T \rangle \\
\equiv & \;\;\;\;\;\text{"logic: $\;\lnot p \lor q\;$ is another way to write $\;p \Rightarrow q\;$"} \\
& \langle \forall x :: x \not\in S \lor x \in T \rangle \\
\end{align}
Combining these, we can simplify even further:
\begin{align}
& S \cap T = \varnothing \;\land\; S \cup T = T \\
\equiv & \;\;\;\;\;\text{"the above two calculations"} \\
& \langle \forall x :: x \not\in S \lor x \not\in T \rangle \;\land\; \langle \forall x :: x \not\in S \lor x \in T \rangle \\
\equiv & \;\;\;\;\;\text{"$\;\land\;$ distributes over $\;\forall\;$"} \\
& \langle \forall x :: (x \not\in S \lor x \not\in T) \;\land\; (x \not\in S \lor x \in T) \rangle \\
\equiv & \;\;\;\;\;\text{"$\;\lor\;$ distributes over $\;\land\;$"} \\
& \langle \forall x :: x \not\in S \lor (x \not\in T \land x \in T) \rangle \\
\equiv & \;\;\;\;\;\text{"contradiction; simplify $\;p \lor \text{false}\;$ to $\;p\;$"} \\
& \langle \forall x :: x \not\in S \rangle \\
\equiv & \;\;\;\;\;\text{"definition of $\;\varnothing\;$"} \\
& S = \varnothing \\
\end{align}
This proves (a stronger version of) the original statement.
A: Informally, assume that S is non-empty. Then $S \cup T$ is not T, which contradicts the assumption.
