The class of all hereditarily countable sets can be proven to be a set from the axioms of Zermelo–Fraenkel set theory (ZF) without any form of the axiom of choice, and this set is designated . The hereditarily countable sets form a model of Kripke–Platek set theory with the axiom of infinity (KPI), if the axiom of countable choice is assumed in the metatheory. If $x \in H_{\aleph_1}$, then $L_{\omega_1}(x) \subset H_{\aleph_1}$.
What is $L_{\omega_1}(x)$? I heard of constructible universe, but that did not contain a thing like $(x)$....