Let $\phi$ be a formula defining an equivalence relation.
Definitions:
- The $\phi$-cardinality of a set $X$ be the cardinality of $X/\phi$. That is, the cardinality of the set of all equivalence classes of elements of $X$ under equivalence relation $\phi$.
- A set is $\phi$-discriminative if and only if no two distinct elements of it fulfill $\phi$.
Discriminative Choice: For any family $F$ of pairwise disjoint nonempty sets, if the cardinality of $F$ is smaller than or equal to the $\phi$-cardinality of each of its elements, then there is a $\phi$-discriminative set $X$ that shares exactly one element with each element of $F$.
Is discriminative choice provable in $\sf ZFC$?