I am wondering about whether it is possible/makes sense that you could use the fact of semantic entailment (or logical consequence) in a formal proof?
Consider the example: Suppose $A \cap C \subset B$ and $a \in C$. Then $a \notin A\backslash B$. It is straightforward to prove by turning the negation into an implication and just directly proving it. In this example, I can imagine how these steps, starting from the premises, could be written out formally starting with the premises and using rules of inference to arrive at the next sentence, step-by-step until I arrive at the final sentence.
However I was wondering about what happens if instead you follow this sequence of logical inference until you arrived at the following (very contrived) sentence: $$\forall x [x \in A \land x \in C \implies x \in B] \land a \in C$$
Up until this sentence it seems to me that there would be a way of using logical inferences to get here from the premises. Here is where my question came from: It seems to me that by assuming cases for $a \in A$ and it's negation, we can show the conclusion. I.e.
If we assume $a \in A$ then we have $a\in A \land a \in C \rightarrow a \in B$, and
if we assume $a \notin A$ then we have $a \notin A$
To finally arrive at $a\notin A \lor a \in B$, which is exactly the conclusion.
However I don't know if this reasoning works in a logical proof. The cases I considered have the form $A$ and $\neg A$.So consider the truth table for $A \lor \neg A$, $P$, $Q$, and $P \lor Q$, and where we know that $A \vdash P $ and $\neg A \vdash Q$, where here $P$ and $Q$ could represent the statements $a \notin A$ and $a \in B$ respectively.
From the truth table (or quite obviously anyway), I can see that $P \lor Q$ is a logical consequence of $A \lor \neg A$. In other words, $(A \lor \neg A) \vDash (P \lor Q)$.
My understanding is that a formal proof is a sequence of sentences, which are derived from the rules of inference of our formal system. I have recently learnt the distinction about the difference between metalanguage and language of the formal system, and the semantic entailment does not seem to be a logical inference rule (at least of propositional calculus).
So ultimately my question is whether I can use the fact that $(A \lor \neg A) \vDash (P \lor Q)$ in a formal proof? For example, could I in the proof assume $A \lor \neg A$ (which I assume is valid since it is a tautology), and then state "since $(A \lor \neg A) \vDash (P \lor Q)$ , $P \lor Q$"
My apologies if I am misunderstanding the notions here, I only have a shallow understanding of logic so I am not sure if this answer is obvious either way.