Definable subsets of a constructible level are small

Put $\kappa =\mathrm{\mid }\alpha \mathrm{\mid }$ and fix a bijection from $L_{\alpha }$ to $\kappa$ using F2. Iterate one pairing bijection from F4 and encode lengths to inject all formula/finite-tuple pairs into $\kappa$. Each definable subset has a code by F1. Its least code exists; assigning that code gives an injection $\mathrm{Def}(L_{\alpha })\to \kappa$, hence a well-order and an upper bound by F3. Empty parameter tuples are among these codes.

For every $a\in L_{\alpha }$, transitivity from F5 gives $a\subseteq L_{\alpha }$; the formula $x\in a$ with the single parameter a defines exactly a over $L_{\alpha }$. Thus $L_{\alpha }\subseteq \mathrm{Def}(L_{\alpha })$, providing a lower bound of $\kappa$ by F2.

Both sets are well-orderable by step 1.1 and F2. The upper and lower bounds therefore give $\mathrm{\mid }\mathrm{Def}(L_{\alpha })\mathrm{\mid }=\kappa =\mathrm{\mid }\alpha \mathrm{\mid }$. The only selections in the proof were one bijection for the already well-orderable level and one cardinal pairing; least codes supply all subset representatives without AC.