Existence of generic filters when forcing with a class of conditions.

Question

As the title says, suppose we have a countable transitive model of ZFC like $M$ and suppose $\mathbb{P}$ is a class partial order in $M$. My question is how can we prove that the cardinality of definable classes over $M$ is countable? Do we have to formalize logic in ZFC and use the fact that the number of formulas with free variables in $M$ is countable? If so, can you please guide me on how to do this formally? If not, is there another simpler method? Thanks for your patience.

Answer 1

Well.

A definable class is given by a formula and a tuple of parameters (we can in fact assume it is a single parameter by the fact a tuple is in fact an object in the model). The language is countable, so there are only countably many formulas. If the model is countable, so there are only countably many tuples of objects.

In particular, there are only countably many classes.