Can I prove set propositions using first-order logic? I'm studying logic and sets and I have to say there's a strong similarity between the two. Most boolean/logic axioms also apply to sets. At the end of my course I also studied first-order logic (or predicate logic) and how one can actually define statements using first-order logic. This was quite a revelation to me because it is quite easy to prove first-order logic statements compared to set propositions (my brain just works better at decomposing first-order logic propositions). So I'm wondering, is it possible to prove set propositions using first-order logic? Here's an example of a set proposition I have to prove:
if C ⊆ B then A ⇒ C ⊆ A ⇒ B 
(not that A ⇒ B is assumed to mean ¬A ∪ B)
Now I was thinking I could convert this into a first-order logic statement, such as: 
Subset(C, B) ⇒ Subset(A ⇒ C, A ⇒ B)
As you can see however I can't seem to understand how to prove that in first-order logic. Anyway, perhaps I am confusing the two and this is not possible but I was wondering what you guys thought about proving these set statements using first-order logic.
 A: You can translate between set algebra and logic, but you need to speak about elements in order to do so.
If you take a set algebra expression, you can rewrite it into set-builder notation from the bottom up as follows:


*

*A named set $A$ is the same as $\{x\mid x\in A\}$.

*For a union, first rewrite the operands until they have set-builder form, and then use $$ \{x\mid \phi(x) \} \cup \{x\mid \psi(x) \} = \{x\mid \phi(x)\lor\psi(x)\} $$ where $\phi(x)$ and $\psi(x)$ are some formulas that have $x$ free.

*Similarly, intersections and complement correspond to conjunction and negation:
$$ \{x\mid \phi(x) \} \cap \{x\mid \psi(x)\} = \{x\mid \phi(x)\land\psi(x) \} \\ \{x\mid \phi(x) \}^\complement = \{x \mid \neg \phi(x) \} \\
\{x\mid \phi(x) \} \setminus \{x\mid\psi(x)\} = \{x\mid \phi(x)\land\neg\psi(x)\} $$

*When you have a relation between sets, you get plain logical formulas back:
$$ \{x\mid \phi(x) \} \subseteq \{x\mid \psi(x)\} \iff \forall x (\phi(x)\rightarrow \psi(x)) \\
\{x\mid \phi(x) \} = \{x\mid\psi(x)\} \iff \forall x(\phi(x)\leftrightarrow \psi(x)) $$
It seems you already have this kind of translation in mind when you're using "$\Rightarrow$" and "$\neg$" as set algebra operations -- these symbols are usually used only as logical connectives. (Conversely, there is no conventional logical connective that by itself represents set difference).
The underlying similarity here is that the universe of sets with $\cup$, $\cap$, $\complement$, or the universe of formulas with $\lor$, $\land$, $\neg$ both constitute Boolean algebras. The $\{x\mid\cdots\}$ construction is a homomorphism between the two Boolean algebras, and the work mostly just consists of changing notation to that used on the other world.
A: You can convert many set theoretic statements to Boolean expressions.  The most important thing to note is that the set $A$ is not appropriate for a Boolean expression because it's not a statement.  You should replace $A$ with $x\in A$ because $x\in A$ can be true or false.  The translations are as follows:
$$
\begin{array}{c|c}
\text{Set}&\text{Boolean}\\\hline
A\subseteq B&x\in A\Rightarrow x\in B\\
A^c&\neg(x\in A)\\
A\cap B&(x\in A)\wedge (x\in B)\\
A\cup B&(x\in A)\vee (x\in B)\\
A\setminus B&(x\in A)\wedge (x\not\in B)
\end{array}
$$
From this list, you can derive most statements in basic set theory (but some get very complicated to compute).
Notes: $A^c$ is the complement of $A$ in some universe.  $\neg(x\in A)\equiv x\not\in A$.
