Solution (source code)

= Solution

Equality with the <union> is expressed by
$$
\boxed{\bigl(\forall z\in x\ \exists u\in y\ z\in u\bigr)\ \land\ \bigl(\forall u\in y\ \forall z\in u\ z\in x\bigr).}
$$
The first conjunct says that every member of $x$ lies in some member of $y$; the second gives the reverse inclusion. Every <quantifier> is bounded by a parameter or by an element of a previously bounded parameter. Therefore bounded absoluteness applies, proving full absoluteness and hence upward absoluteness of $x=\bigcup y$. This only compares the relation for existing parameters; it does not require either class to contain the <union> of every one of its <sets>.