Consider
Lemma. Let $A$ be a set. Then there exists a set $B$ such that $A$ and $B$ are disjoint and a bijective function $A\to B$.
Remark: In order to minimize the axioms needed to even speek of function graphs, the function shall be given by a formula $\phi(x,y)$ with the obvious properties $\forall a\in A\exists !b\in B\colon \phi(a,b)$ and $\forall b\in B\exists !a\in A\colon \phi(a,b)$. I'd prefer to avoid it, but in some cases it may be helpful to additionally equip $\phi$ with a parameter.
Background: This lemma is often useful when constructing an extension of some kind of a set (e.g., $\Bbb Z$ from $\Bbb N$ as a set of equivalence classes of pairs, or $\Bbb R$ from $\Bbb Q$ as Dedekind cuts) and for formal reasons one wants to have the original set (instead of an isomorphic image) actually as s subset of the extension.
A typical way to show the lemma would be to let $B=\{\,\{a,\{A\}\}\mid a\in A\,\}$ and the bijection of course $a\mapsto \{a,\{A\}\}$, here expressed as (avoiding the use of $A$ as a parameter) $$\phi(a,b)\equiv \exists c\colon b=\{a,\{c\}\}.$$ The construction of $B$ uses Pair and Replacement, the proof of disjointness uses Foundation, and I guess that the proof of bijectivity of the map does not need more than these (or probably "unconciously" Extensionality somewhere in the background).
Question: Which other minimal subsets of the usual ZFC axioms (counting axiom schemas as one) can be used to show the lemma? E.g., can we get rid of Foundation by using Powerset? While $P(A)$ is big enough to contain a suitable $B$, too much additional machinery may be needed to show the existence or explicitly come up with a $\phi$ or show its validity. Also of interest: Is there such a minimal set with Choice in it (in which case you may want to add a choice function as parameter to $\phi$)?
Let $A$ be a set.
I want $B$ to be of the form $\{\{a,b\}:a\in A\}$ for some fixed $b$. To have $B$ be disjoint from $A$, it must be the case that $\{a,b\}\notin A$ for every $a\in A$. One way to satisfy this would be to have $b\notin\bigcup A$. That is to say, with the axiom of union and separation we can define $b:=\{x\in\bigcup A:x\notin x\}$. However, I will choose a $b$ so that $b$ additionally satisfies $b\notin A$. This can be done by defining $b$ to be instead $\{x\in (\bigcup A)\cup A:x\notin x\}$, where $S\cup T:=\bigcup\{S,T\}$ thereby officially using the axiom of pairing which would've been required at some point given how I want $B$ to be defined.
I want to find a desired bijective formula. Define the formula $\varphi$ with free variables $x$ and $y$ by
$$\begin{align} \varphi(x,y):=(y=\{x,b\}) \end{align}$$
By the axiom of extensionality, $\varphi$ is function-like. Additionally, if $\{a_0,b\}=\{a_1,b\}$ for some $a_0,a_1\in A$, then because $b\notin A$ it follows that $a_0=a_1$. Therefore $\varphi$ is injective-like when defined on $A$.
The last step would be to construct $B$. One easy way would be to invoke replacement, but I have a preference towards the powerset/separation combo axioms. Define
$$B:=\{p\in\mathscr{P}(A\cup\{b\}):(\exists a\in A)(\exists \hat{b}\in\{b\})[p=\{a,\hat{b}\}]\}$$ thereby officially using the axiom of power set.