Cohen's first non-AC model, the one with a Dedekind-finite infinite set $A$ of reals, can be defined in two ways, 1st, as $HOD(A)$ in a bigger generic model of ZFC (the one obtained as a generic extension of $L$ via the countable product of the Cohen forcing), and 2nd, via symmetric names. Jech notes in one of his books that both methods yield exactly same models. I wonder is there any consistent proof somewhere as a source of reference?