Let $M$ be a transitive $\in$-interpretation of a extension $T$ of $ZF$ in $ZF$,and let $B$ such that $$T\vdash B\in M\wedge B\text{ is a complete Boolean algebra}$$ Then, using the fact that any set can be well-ordered in $M$, for a ultrafilter $G$ of $B$, the following are equivalent:
- $G$ is a $M$-generic (i.e. for any $A\subseteq G$, $\bigwedge_{a\in A}a\in G$);
- For any anti-chain $A$ of $B$, such that $\bigvee_{a\in A}a=1$, there is a unique $a\in A\cap G$ (i.e. for any partition of unit of $B$, there is a unique $a\in A\cap G$).
For $(1)\Rightarrow (2)$ there is no need of AC. Is there a way to prove $(2)\Rightarrow (1)$ without the validity of AC in $M$?
I want use the above equivalence to prove that, for any names $\underline{x},\underline{y}\in M^{(B)}$ of $x,y\in M[G]$, respectively, $$(x\in y)\leftrightarrow ||x\in y||\in G,$$ and $$(x = y)\leftrightarrow ||x=y||\in G.$$
Let me answer your underlying question. You don't need the axiom of choice. The proof in Jech "Set Theory" (3rd edition) of this claim, which is Lemma 14.28 is a choice free proof. As is the following theorem which extends that to arbitrary statements in the language of forcing (not just atomic ones).
It's really just by induction on the maximal rank of the names for $x$ and $y$, doing both things simultaneously.