Big intersection operation According to "Elements of Set Theory" 30p,

$$\emptyset \neq A \subseteq B \;\,\Rightarrow \;\, \bigcap B \subseteq \bigcap A.$$
In each case, the proof is straightforward. For example, in the last case, we assume that every member of $A$ is also a member of $B$. Hence if $x \in \bigcap B$, i.e., if $x$ belongs to every member of $B$, then a fortiori $x$ belongs to every member of the smaller collection $A$. And consequently $x \in \bigcap A$.

I wonder if the last part is really a proof. It is okay to assume $x \in \bigcap B$ and arrive at $x \in \bigcap A$. But can I use this reasoning "then a fortiori $x$ belongs to every member of the smaller collection" in a proof exercise? It looks like just using intuition (it does not seem rigorous).
 A: I do not agree. It is a very rigorous argument, and I cannot see how it could be made more formal. Indeed, the proof assumes that $A\subseteq B$, which means that (I quote from the proof)

every member of $A$ is also a member of $B$.

From that and from the fact that "$x$ belongs to every member of $B$", it follows immediately that, in particular, "$x$ belongs to every member of $A$". It is just a syllogistic inference roughly of the form "if $X$ implies $Y$ and $Y$ implies $Z$, then $X$ implies $Z$", which does not require any further justification.
A: In case it helps, here is a different style of proof of the same.$%
\require{begingroup}
\begingroup
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\then}{\Rightarrow}
\newcommand{\when}{\Leftarrow}
%$
For all $\;x\;$, we have
$$\calc
  x \in \bigcap A
\op{\equiv}\hint{definition of $\;\bigcap\;$}
  \langle \forall S :: S \in A \;\then\; x \in S \rangle
\op{\when}\hints{$\;A \subseteq B\;$, so by the definition of $\;\subseteq\;$,}
          \hint{$\;T \in A \then T \in B\;$ for any $\;T\;$; logic}
  \langle \forall S :: S \in B \;\then\; x \in S \rangle
\op{\equiv}\hint{definition of $\;\bigcap\;$}
  x \in \bigcap B
\endcalc$$
Or equivalently, by the definition of $\;\subseteq\;$, $\;\bigcap B \subseteq \bigcap A\;$.
Note that weakening the antecedent of $\;\then\;$ (from $\;S \in A\;$ to $\;S \in B\;$), causes the expression $\;S \in A \;\then\; x \in S\;$ as a whole to be strengthened, and therefore the middle step uses $\;\when\;$, 'flipping' the direction of the implication.
$%
\endgroup
%$
