Proof-making for "A Set is a Subset of Itself" / Law of Identity. Recently I've been trying to figure out a proof regarding set theory, for the following theorem:
"A set is a subset of itself" or $∀x:S ⊆ S$, or:
$∀x:  (x∈S ⟹    x∈S)$
ProofWiki states that such a problem can be solved with the law of identity, but I do not understand how that works, as such a law is only used with conjunctions and disjunctions, and not conditional statements. I figure I could do something using the definition of a subset but I do not know where to go from there. Any help would be appreciated. Thanks!
 A: The usual axioms of first-order logic with equality are (the generalization of) :

$x = x$;
$x = y \to (\alpha \to \alpha')$, where $α$ is atomic and $α'$  is obtained from $α$ by replacing $x$ in zero or more (but not necessarily all) places by $y$

[see Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112].
In set theory the atomic formulae are precisely the formulae : $x \in s$.
Thus, applying the second axiom with the formula $x \in s$ as $\alpha$, we get :


$x=x \to (x \in s \to x \in s)$.


Then, using the first axiom : $x=x$, we can "detach" : $(x \in s \to x \in s)$ and finally we "generalize" it to conclude with :

$\forall x (x \in s \to x \in s)$.


See also Application to Equality of Sets of Leibniz's Law.
A: The "Law of identity", as given in ProofWiki, is that $$p\implies p$$ for any formula $p$.  Here the formula is $x\in S$, and by the law of identity, $$x\in S \implies x\in S$$ which is what you want.
A: The name "law of identity" is sometimes (and in particular on ProofWiki) used to denote the rule that
$$ P \Rightarrow P $$
is always valid for every formula $P$. That is, anything implies itself.
In your case, if we let $P$ be the formula $x\in S$, we get a proof of
$$ x\in S \Rightarrow x\in S $$
and the rule of generalization (in whichever form it exists in your particular logical system) then allows us to conclude
$$ \forall x (x\in S\Rightarrow x\in S) $$
which is exactly what "$S\subseteq S$" is an abbreviation for.
