In "Modern Algebra" by Seth Warner (1965), section 8 (page 54 in my copy) there exists this:

"If $\displaystyle E$ and $\displaystyle F$ are sets, then there is a bijection from $\displaystyle F$ onto a set $\displaystyle F'$ disjoint from $\displaystyle E$."

It also says: "[This] may be proved in any formal development of the theory of sets."

But I haven't found this proof anywhere, so I'm trying to craft my own proof.

My approach is as follows.

Let $\displaystyle f: F \to F$ be a bijection, any bijection (the identity mapping will do).

If $\displaystyle E \cap F = \varnothing$ then job done, $\displaystyle F = F'$ and $\displaystyle f$. is our bijection.

Otherwise we have to construct it, or prove that there is a process for doing so.

Take $\displaystyle S = E \cap F$, and put all elements of $\displaystyle F - E$ into $\displaystyle F'$.

Let $\displaystyle P(S)$ be the power set of $\displaystyle S$.

Take some element $\displaystyle s \in S$.

Then (as is easily proved) $\displaystyle \exists t \in P(S): t \notin S$. So put $\displaystyle t \in F'$.

Then you create the mapping $\displaystyle f'$ defined as:

$\displaystyle f'(x) = \begin{cases}

f(x) & : x \ne s \\

t & : x = s

\end{cases}$

Then you've got $\displaystyle S' = S - \{s\}$ and you can repeat the process with $\displaystyle S'$.

However, this gets messy when $\displaystyle S$ is infinite (and worse when it's uncountable) and requires the Axiom of Choice in order to construct such a set.

Also, I haven't proved that the $\displaystyle t$ I picked is not already in $\displaystyle F - E$ which would render my mapping $\displaystyle f'$ not a bijection.

Does anyone know of an easier way of doing this? Apologies for any howlers in this, I'm practically self-taught when it comes to set theory.

Please be aware that any proof produced will appear (in some form) on the page:

Exists Bijection to a Disjoint Set - ProofWiki
... so unless you're happy for this to happen, best not answer.