On Disjoint Union

The notation (/definition) of disjoint union seems always to create some confusion in mathematical praxis, here I present briefly the understanding I have of it.

For "$\bigsqcup$" the symbol of disjoint union, I define the following:[^1] $c=a\bigsqcup b:=c=a\cup b\wedge a\cap b=\varnothing$which is a well-defined formula in language of set theory (given the usual notations for "$\cap$", "$\cup$" and "$\varnothing$"). This seems to me not to be that controversial, surprising nor distant from mathematical praxis.

The problems arise when one wishes to talk about $a\bigsqcup b$ without making a formula with it. Then the claim would be that $a\bigsqcup b$ is a well defined. I formally understand this, given the context of my Bachelor Thesis, that $a\bigsqcup b$ has a Complete Description, i.e. ${\exists }_{\phi \in {\mathcal{L}}_{ϵ}}(ZFC⊢\phi (a\bigsqcup b)\wedge {\forall }_x\phi (x)\to x=a\bigsqcup b)$. Now, take the instance where $a=\{\varnothing ,\{\varnothing \}\}$ and $b=\{\varnothing ,\{\{\varnothing \}\}\}$; there $\phi (a\bigsqcup b)$, depending on the definition we wish to have on $\phi$, would admittedly not hold and the term $a\bigsqcup b$, which is hence not defined.

[1]: Recall that "$:=$", being a metalinguistic symbol, has the maximal scope.