Yes, this theory is synonymous with $\sf{ZF}$ plus global choice. Explicitly, we'll prove direct equivalence to the theory: $\sf{ZF}$ plus a global wellorder $<$, plus the following two axioms.
$$\operatorname{rank}(x)\subsetneq \operatorname{rank}(y) \implies x<y \tag{Ax1}$$
$$\sup\{\operatorname{S}(x) : x\in A\}<\sup\{\operatorname{S}(x) : x\in B\} \implies A<B \tag {Ax2}$$
$$\operatorname{S}(x) := \min\{y : x<y\}$$
Basically, axiom 1 just says $<$ is rank-respecting. For any such wellorder, we can also consider the function $A\mapsto \sup\{\operatorname{S}(x) : x\in A\}$, and the universe can be partitioned into a wellordered hierarchy based on the output of that function. Axiom 2 simply says that $<$ respects the aforementioned stratification in the same way that it respects rank.
Once we've proven direct equivalence between your theory and mine, the desired synonymity can be proven using the same basic techniques outlined in this answer by Elliot. Basically, it's not terribly difficult to show that a global choice function can induce a global wellorder obeying my axioms 1 and 2, and there's enough freedom in how each stratum is constructed to produce a bi-interpretation using the same kind of Cantor-Bernstein tactic used by Elliot.
To prove equivalence, we notice that my axiom 1 proves Respective, and moreover that Hyper-respective is logically equivalent to axiom 2, as follows.
$$\begin{align}
&\forall z, (((\forall(m\in x), m<z)\land z\in y) \implies x<y) \\
&(\exists z,(\forall(m\in x), m<z)\land z\in y) \implies x<y \\
&(\exists(z\in y), \forall(m\in x), m<z)\implies x<y \\
&(\exists(z\in y), \sup\{\operatorname{S}(m) : m\in x\}\leq z)\implies x<y \\
&\sup\{\operatorname{S}(m) : m\in x\}<\sup\{\operatorname{S}(m) : m\in y\}\implies x<y
\end{align}$$
The rest of your axioms are trivial consequences of my theory, so mine proves yours. To show that your theory proves mine, we'll show that yours proves all the axioms of $\sf{ZF}$ with a setlike global wellorder. After that, we recover my axiom 2 using the same equivalence just described. Finally, it turns out that my axiom 2 just implies axiom 1 outright, so your theory proves mine. The proof of axiom 1 using axiom 2 is described below, and after that we'll show how your theory proves the axioms of $\sf{ZF}$ with a setlike global wellorder.
Assuming $\sf{ZF}$ with a global setlike wellorder and axiom 2, we prove $\forall x,\forall y, \operatorname{rank}(x)\subseteq \alpha\subsetneq\operatorname{rank}(y) \implies x<y$ for all ordinals $\alpha$, where $\subsetneq$ is (equivalent to) the standard order relation on the ordinals. By contradiction suppose not, then let $\alpha$ be an inclusion-minimal counter example. Since $\operatorname{rank}(y)\supsetneq\alpha$, we can find $t\in y$ with $\operatorname{rank}(t)\supseteq \alpha$. By contrast, all $m\in x$ must have $\operatorname{rank}(m)\subsetneq \operatorname{rank}(x)\subseteq \alpha$. If we label $\beta=\operatorname{rank}(m)$ then $\beta\subsetneq \alpha$, and by minimality of $\alpha$ we infer $\operatorname{rank}(m)\subseteq\beta\subsetneq\operatorname{rank}(t) \implies m<t$, hence we actually have $m<t$ for all $m\in x$. It follows that $\sup\{\operatorname{S}(m) : m\in x\}\leq t < \sup\{\operatorname{S}(t) : t\in y\}$, which guarantees $x<y$ via axiom 2. This contradicts the premise of having a counter example, so no counter examples exist and axiom 1 is proven.
Extensionality and Specification are easy consequences of the Sets and Respective axioms. For any set $y$, there's a unique set $x$ where generally $m\in x \iff (m\not>y \land (m\in y\land \phi))$. Notice that $m\in y \implies m<y \implies m\not>y$, where the first implication follows from Respective, and the second follows from Ordering. This makes the term $m\not>y$ redundant in the earlier formula, so it simplifies to $\exists!x, \forall m, m\in x \iff (m\in y \land \phi)$. The existence of such $x$ implies Specification directly. In the special case where $\phi$ is a tautology, the uniqueness of $x$ implies Extensionality.
To prove $<$ is a global wellorder, we just prove it's trichotomous. Given any $a,b$ such that $\neg(a\leq b)$, use Sets to construct $x=\{m\not>a : m=a\lor m=b\}$. We have $b\not >a$ by premise, and $a\not>a$ by Ordering, so then $x=\{a,b\}$. Now apply Ordering to find $m\in\{a,b\}$ obeying $m\leq a$ and $m\leq b$, and since $\neg(a\leq b)$ then $m=b$ and so $b\leq a$. It follows deductively that $\neg(a\leq b) \implies b\leq a$ for all $a,b$, which is equivalent to Trichotomy. Along with Ordering, this proves $<$ is a global wellorder.
Moreover we see $<$ is setlike, by consequence of Sets. Indeed, for any $n$ we find a set $x=\{m\leq n : \phi\}$, and taking $\phi$ to be a tautology implies $\{m : m\leq n\}$ is a set, so $<$ is setlike.
Pairing is now trivial, $\{x,y\}=\{m\not>z : m=x\lor m=y\}$ where $z=\max(x,y)$.
Regularity is not much harder, as any nonempty $x$ admits $l\in x$ where $\forall(m\in x), l\leq m$, due to Ordering. Since having $m\in l$ would imply $m<l$ via Respective, it follows that $x\cap l = \emptyset$, proving Regularity.
The axiom of Union follows since, for any set $x$, we simply have $u=\{m : m\leq x\}$ being a superset of the union of $x$. Indeed, given $k\in m\in x$ we have $k<m<x$, therefore $k\in u$ implying $m\subseteq u$. All $m\in x$ have $m\subseteq u$, so the union of the members of $x$ is just a subset of $u$.
The axiom of Powerset is a consequence of Hyper-Respective. Take any set $z$, let $y=\{z\}$ which exists via Pairing, then let $p=\{m\leq y : m\subseteq z\}$. Notice that every subset $x\subseteq z$ obeys $\forall(m\in x), m\in z$ and thus $\forall(m\in x), m<z$ via Respective, and since $z\in y$ then $x<y$ via Hyper-respective. It follows that $x\in p$, and so $p$ contains every subset of $z$, proving Powerset.
The schema of Replacement is almost identical to Boundedness. Let $F$ be any function symbol, let $x$ be any set, and let $\psi$ be the predicate coding the class image of $F$ over the set $x$. Using $<$, we can find a subset of $x$ on which $F$ bijects to $\psi$, explicitly $x'=\{m\in x : m=\min\{k\in x : F(k)=F(m)\}\}$. Now $F$ bijects $x'$ with $\psi$, so Boundedness finds $y$ bounding $\psi$. It follows that every $m\in x$ admits $k\in x'$ with $F(m)=F(k)$, and any $k\in x'$ has $F(k)<y$, hence $F(m)<y$. Letting $y'=\{j : y\leq y\}$, we have Replacement since all $m\in x$ have $F(m)\in y'$.
Finally, the Infinity axiom of $\sf{ZF}$ is now a direct consequence of your Infinity axiom. This works because the class $\mathbb{N}$ of finite ordinals can be defined without ever assuming Infinity, and we can also prove the Recursion theorem without ever assuming Infinity, and we have all other axioms of $\sf{ZF}$. Simply let Let $\ell$ denote the minimal $l$ witnessing your Infinity axiom, let $\mathbb{N}$ denote the class of all finite ordinals, then apply Recursion to define a bijection between $\{x : x<\ell\}$ and $\mathbb{N}$ in the expected way. The former is a set, and so the latter is a set via Replacement.
