How to define the domain for such function in ZFC?

Question

Suppose a logical function which takes a set and an element and iteratively tells wether $x$ is inside or not. It is defined as

$$f(S,x)\iff x\in S \bigvee_{A\in S}f(A,x)$$

But how do I define its domain? It is clear what it takes, a set and an element, so it should be something like $f:S'\times X\to \mathbb{B}$ where $S'$ is the set of all sets(?) and $X$ the set of all elements(?). Clearly, these sets does not exist in ZFC, but the function yes, and I really need to define its domain. How can I do it?

I thought about $(S,x)\mapsto b$, but useful info gets hidden, which I dont want.

Answer 1

Rather than "logical functions," it's better to just think of formulas. You have a formula here of two variables. That said, if you really want to think of it as a function, it's a class function like the "function" $x\mapsto \{x\}$, and its domain is a proper class (namely, the whole set-theoretic universe).

As a side note, it's more succinct to say "$f(x, S)\iff x\in tcl(S)$" (where "$tcl$" denotes the transitive closure).

Answer 2

Letting $V$ denote the type of all sets, the domain of $f$ would be the type $V \times V$.

Note in ZFC there is no distinction between "set" and "thing which can be an element".