I am taking a course on mathematical logic and am struggling to give formal proofs of theorems or claims. Currently doing first order logic. Here, an example:
Claim: $\models (\exists x)\big(A(x)\Rightarrow (\forall y)(A(y))\big)$
where $A$ is an unary predicate. I am asked to prove this. This is how I would reason:
By the rule of propositional logic $P\Rightarrow Q$ is equivallent to $\neg P\vee Q$. So we wish to show that $$\models(\exists x)\big(\neg A(x)\vee (\forall y)(A(y))\big)$$ So, assume we have an arbitrary interpretation of language $\mathcal{L}=\{A\}$, that is a nonempty set $M$ together with unary predicate $A$.. By Tarski's definition of truth, there is some $m\in M$ for which is $\neg A(m)$ or for all $n\in M$ $A(n)$ holds. But this is clearly true (logically valid). Because whenever there is some $m\in M$ for which $\neg A(m)$, then the formula is satisfied. If not, then for all $n\in M$ for which $A(n)$, which makes it also satisfied.
Now, I am wondering whether this can be taken as a formal proof of the claim that the formula is logically valid in any interpretation of the language $\mathcal{L}=\{A\}$. It seems really trivial, but I am afraid I am using too much of set theory.
Another reasoning could be: In fact, when $A$ is an unary predicate, that means $A$ is a subset of $M$. Now distinguish two cases: 1. $A=M$, then $(\forall y)((y\in M) \Leftrightarrow (y\in A))$ in other words $(\forall y)(A(y))$. If $A\subsetneq M$ then it is clear there is some $m\in M$ that is not in $A$, in this case the part $(\exists x)(\neg A(x))$ is true. Now, this uses the definition of equality between sets and what is a subset.
Another idea: Using a contradiction. Assume this was not logically valid, so there exists some interpretation $\mathcal{M}$ and value assignment $e$ for which $\mathcal{M}\models \neg(\exists x)\big(A(x)\Rightarrow (\forall y)(A(y))\big)$, that is $\mathcal{M}\models(\forall x)(A(x)\wedge (\exists y)(\neg A(y))$, thus for all $m$ $\mathcal{M}\models A(m)\wedge (\exists y)(\neg A(y))$, by definition again there is some $n\in M$ for which $\mathcal{M}\models A(m)\wedge \neg A(n)$, this gives $\mathcal{M}\models A(n)$ (the $n$ must be one of all of the $m$'s) but also $\mathcal{M}\models \neg A(n)$. Which is contradiction by the law of excluded middle, so the statement before was logically valid.
Or just by looking: It is clear that either for all $x$ $A(x)$ holds, or there is some $x$ for which $A(x)$ doesn't hold...
All this seems like a handwaving...
So, what tools/methods/kind of reasoning should I use at most when proving such claims and theorems in logic/model theory? I would be grateful for opinions and/or more examples (sources).