Link existential to cardinality

[wdcraft01]

It could be useful to have a theorem directly linking an existential claim such as:

$\exists_{x \in S} [ Q(x) ]$

to the logically equivalent set theory claim that

$\big| \{x \,|\, Q(x) \}_{x \in S} \big| \ge 1$

A related situation has recently come up in work in the QEC branch, where I am trying to streamline some proof steps in which we first show that there exists at least one odd vertex in the graph of an error, then eventually prove that the odd vertex must be a boundary vertex and that there are actually exactly two such odd boundary vertices.

I would propose the following theorem, placed at the top level of the logic package (since it relates logic/booleans/quantification/existence to logic/sets/cardinality and logic/sets/comprehension/set_of_all):

$\forall_{x \in S} \big[ \forall_{Q} \big[ (\exists_{x \in S} Q(x)) = (\big| \{x \,|\, Q(x) \}_{x \in S} \big| \ge 1) \big]\big]$