Some properties of $L[A]$ (Constructible universe relativized to $A$)

Question

Question
We defined $L[A]$, constructible universe relativized to $A$ (definition below) and should now prove the following properties:
1. $L[A]$ is transitive.
2. All axioms of $ZF$ hold in $L[A]$.
3. If $A$ is a set of ordinals, then the Axiom of Choice holds in $L[A]$.
4. Let $\bar{A} = A ∩ L[A]$. Then $L[\bar{A}] = L[A]$ and moreover $\bar{A} ∈ L[\bar{A}]$.

What I know
I allready know that the properties 1.-3. hold in $L$, so I think I just need to show that they are definable in $A$. Is this right? But I am stil not sure how to do that. And for 4. I have no clue how to prove that.

Definition
Given a set $A$ and a transitive model $M$, we set \begin{equation} def_A(M) = \{X ⊆ M : X \text{ is definable over } (M, ∈, A ∩ M) \text{ with parameters from } M\} \end{equation} where $A ∩ M$ is allowed as an additional unary predicate in the model. We defined \begin{align} L_0[A] &:= \emptyset, \\ L_{\alpha + 1} [A] &:= def_A(L_{\alpha}[A]), \\ L_{\lambda} [A] &:= \bigcup_{\alpha < \lambda} L_{\alpha} [A], \\ L[A] &:= \bigcup_{\alpha \in ON} L_{\alpha} [A]. \end{align} Here $\lambda$ is a limit Ordinal and $ON$ denotes the class of all Ordinals.

Answer 1

You need to literally repeat the same proof as you would have in the construction of $L$. There's no funny business about it.

For the 4th item:

1. Prove by induction that $L_\alpha[A]=L_\alpha[\overline A]$,
2. then conclude that there is some $\alpha$ such that $\overline A=A\cap L_\alpha[A]$ and it is a subset of $L_\alpha[A]$,
3. finally, use the definition of $L_{\alpha+1}[A]$ to conclude that $\overline A\in L[\overline A]=L[A]$.

Answer 2

I'm not sure how to interpret your idea, so let me leave a few instructions instead:

1. Prove, by induction on $\alpha$, that $L_{\alpha}[A]$ is transitive. For $\alpha = 0$ and $\alpha$ limits the induction step is trivial. For successor ordinals $\alpha = \beta +1$ you adapt the computation for $L$ to this case (it's basically the same proof).
2. The inner model criterion comes in handy here: Show that $L[A]$ is closed under Gödel operations and almost universal. If you don't know the criterion or these terms, have a look at Theorem 13.9 of Jech's 'Set Theory -- 3rd millenium edition'. (It's a very handy tool to have, so it's worth your time learning about it regardless.)
3. Adapt the usual construction of a global well-order for $L$. The key is that $L[A]$ contains a well-order for $A$ (the membership relation) in case that $A$ is a set of ordinals.
4. Asaf handled this.