Some properties of $L[A]$ (Constructible universe relativized to $A$) 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.
 A: 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:


*

*Prove by induction that $L_\alpha[A]=L_\alpha[\overline A]$, 

*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]$, 

*finally, use the definition of $L_{\alpha+1}[A]$ to conclude that $\overline A\in L[\overline A]=L[A]$.

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


*

*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).

*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.)

*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.

*Asaf handled this.

