Is there any standardized "practical extension" language for ZFC?

Question

It seems that in practical proofs regarding ZFC, we use not the strict first-order language of ZFC but an extension which allows for terms including enumerated sets, unions, selection sets, etc. I was wondering if there was any formal language that was standardized to enable formalizing such proofs.

What I was thinking of would be something along these lines. Here, $prop_n$ would represent propositions with $n$ (possibly) free variables, $term_n$ would represent terms in $n$ (possibly) free variables, and $termlist_n$ would represent lists of terms in $n$ (possibly) free variables. Also, in order to avoid specifications of what variables would have to be free or not free where in the associated logical rules, I tend to like using de Bruijn indices. (Note that the below is not meant to be interpreted as a grammar for parsing strings into propositions or terms, but as a description of the possible nodes of an abstract syntax tree.)

\begin{align*} prop_n \leftarrow & term_n \in term_n \\ | & term_n = term_n \\ | & \top \\ | & \bot \\ | & prop_n \wedge prop_n \\ | & prop_n \vee prop_n \\ | & prop_n \rightarrow prop_n \\ | & \forall \cdot, prop_{n+1} \\ | & \exists \cdot, prop_{n+1} \\ term_n \leftarrow & v_i \mathrm{~where~}0 \le i < n \\ | & \{ termlist_n \} & \mathrm{(enumerated~set)} \\ | & P(term_n) \\ | & \bigcup (term_n) \\ | & \{ \cdot \in term_n \mid prop_{n+1} \} & \mathrm{(selection~set)} \\ | & \{ term_{n+1} \mid \cdot \in term_n \} & \mathrm{(replacement~set)} \\ | & \mathrm{the~unique} \cdot \mathrm{s.t.~} prop_{n+1} \\ | & \omega \\ termlist_n \leftarrow & \\ & | term_n [, term_n]^* \end{align*}

(The "the unique $\cdot$ s.t. $\ldots$" operator would be used fairly early for example in defining how to apply a function specified as a set to an input.)

Then, based on these fundamental proposition and term constructors, we could define further syntactic sugar, for example $\lnot p := (p \rightarrow \bot)$, $X \cup Y := \bigcup(\{ X, Y \})$, $X \cap Y := \{ \cdot \in X \mid v_0 \in Y{\uparrow} \}$ where $Y{\uparrow} := Y[v_0 := v_1, \ldots, v_{n-1} := v_n]$ represents the "lifting" of the term $Y$ to one more free variable, etc.

The intention here would be to show this language with the appropriate axioms (or we could even convert many of the axioms to introduction/elimination rules of a natural deduction proof system) is a conservative extension of strict ZFC, and then use this language as a more practical alternative in formalizing ZFC proofs in a way closer to how they would actually be written.

Now, to reiterate the main question: Is there any existing standardized formal language along these lines?

Answer 1

Z notation is a standardized notation for set theory that is used by several tools as an input language.

Mizar is an implementation of Tarsk-Grothendieck set theory (an extension of ZFC). It has its own meta-notation that allows defining (meta-)functions, predicates, and axiom schemes. From there it defines usual concepts, e.g. $\{y\}$ and union are defined here.

Metamath is a fairly generic metalanguage but has descriptions of set theory. Metamath works at a very low-level syntactic level, so much of what appears to be built-in is actually defined. Variable distinctness is a core, primitive notion in Metamath.

TLA+, Alloy and many other tools used for formal specifications by software engineers are based on set theory and thus provide formalized syntaxes.

Various type theories, dependent and non-dependent, can also "host" a set theoretic language or be used as an alternative. For example, here's ZFC encoded in Twelf, a minimalist dependent type theory used as a logical framework. Twelf, in particular, is not that geared toward syntactic flexibility, but many richer languages, e.g. Agda and Coq, provide more flexibility there. Nevertheless, the host language allows what's called higher-order abstract syntax which offloads the handling variable binding to the host language. For example, $\{x\in A\mid P(x,y)\}$ would be something like restrict A ([x] P x y). You would not have to worry about a substitution for $y$ capturing $x$ as that would be handled by the host language.