$\let\itp\vartriangleright\def\mr{\mathrm}\DeclareMathOperator\dom{dom}\let\bez\smallsetminus\let\sset\subseteq$The weakened theory is much weaker than bounded arithmetic.
Let me denote the theory as $\mr{WT}$. Notice that the weakened comperehension schema is simply equivalent to the schema
$$\tag{$V_n$}\forall w_1,\dots,w_n\,\exists x\,\forall y\,\Bigl(y\in x\leftrightarrow\bigvee_{i=1}^ny=w_i\Bigr)$$
for $n\in\omega$ (here $V_0$ asserts the existence of the empty set). Indeed, by excluded middle, $\{y:(y=w_1\lor\dots\lor y=w_n)\land\phi\}$ is one of the $2^n$ classes $\varnothing$, $\{w_1\}$, $\{w_2\}$, $\{w_1,w_2\}$, $\{w_3\}$, ..., $\{w_1,w_2,\dots,w_n\}$, each of which is a set by $V_n$.
Let $\mr{WT}_k$ denote the finite fragment of $\mr{WT}$ with axioms $V_n$ only for $n\le k$ (it is enough to take $V_0\land V_k$).
First, $\mr{WT}$ is at most as strong as bounded arithmetic. Note that all reasonable fragments of bounded arithmetic are mutually interpretable with Robinson’s arithmetic $Q$, hence I will use that as a gauge.
Theorem 1: $\mr{WT}$ is interpretable in $Q$ (which I will henceforth write as $Q\itp \mr{WT}$).
Proof sketch: Let us start by interpreting in $Q$ a decent fragment of arithmetic such as $S^1_2$. Inside this theory, we can define a well-behaved coding of sequences e.g. as follows: we first represent a sequence $\langle x_0,x_1,\dots,x_n\rangle$ by a string over the alphabet $\{0,1,2\}$ as $2_\smile x_0{}_\smile2_\smile x_1{}_\smile\dots_\smile x_n$ where each $x_i$ is written in binary (with no leading $0$s), and then we reinterpret the string as an integer written in ternary. Using this, we represent finite sets of numbers by strictly increasing sequences. We define $x\in y$ in accordance with this encoding scheme; if $y$ is not a valid representation of a set, we put $x\in y\iff x\ne y$ in order to maintain extensionality. We define $y\mathrel Sx$ as the usual successor relation $y=x+1$. Then it is routine to check that all axioms of $WT$ are valid under this interpretation. QED
We aim to show that $\mr{WT}$ is in fact strictly weaker than $Q$ in terms of strength, i.e., $\mr{WT}\not\itp Q$. To this end, we will relate $\mr{WT}$ with other theories.
Vaught’s set theory $\mr{VS}$ is a theory in the language of set theory $\langle\in\rangle$, axiomatized just by the schema $V_n$ for $n\in\omega$. Let $\mr{VSE}$ denote $\mr{VS}$ + the extensionality axiom. I will write $\mr{VS}_k$ and $\mr{VSE}_k$ for the finite fragments of $\mr{VS}$ and $\mr{VSE}$ (resp.) with $V_n$ axioms only for $n\le k$.
As mentioned in Visser [1,§3], $\mr{VS}$ interprets Robinson’s theory $R$, and as such it is essentially undecidable, however all finite fragments $\mr{VS}_k$ are interpretable in $\mr{VS}_2$, which is just a theory of unordered pairs (denoted $\mr{PAIR_{uno,ns}}$ in [1]); in particular, since there are decidable theories with pairing, it follows that each finite fragment of $\mr{VS}$ has a decidable extension. Consequently, $\mr{VS}\not\itp Q$, and more generally, $\mr{VS}$ does not interpret any finitely axiomatizable essentially undecidable theory.
Notice that $\mr{VSE}$ is a subtheory of $\mr{WT}$. We will show that these two theories are close enough to each other, and generalize to them the results above: finite fragments of $\mr{WT}$ are interpretable in finite fragments of $\mr{VSE}$, and both have decidable extensions.
Theorem 2: $\mr{WT}$ is locally interpretable in $\mr{VSE}$. Specifically, $\mr{VSE}_k\itp\mr{WT}_k$.
Proof: In $\mr{VSE}_k$, we can use the standard Kuratowski pairing function $\langle x,y\rangle=\{\{x\},\{x,y\}\}$ to define $(k+1)$-tuples as $\langle x_0,\dots,x_k\rangle=\langle x_0,\langle x_1,\langle\dots\rangle\rangle\rangle$. Let us put
$$\begin{align}
x\in^*y&\iff\begin{cases}x\in y&\text{if }|y|\le k,\\x\ne y&\text{otherwise,}\end{cases}\\
y\mathrel{S^*}x&\iff\exists\text{ distinct }x_0,\dots,x_k\:(x=\langle x_0,\dots,x_k\rangle\land y=\langle x_1,\dots,x_k,x_0\rangle).
\end{align}$$
It is easy to see that under this interpretation, axioms of $\mr{VSE}_k$ are valid. Since $S^*$ consists of a nonempty collection of $(k+1)$-cycles, the axioms of Existence, Succession, and Uniqueness also hold. Finally, Well-foundedness also holds: any counterexample would have to include at least one full $S^*$-cycle, but none of the infinitely many elements that are not part of any cycle. However, all sets under the interpretation have either at most $k$ elements, or include all but one elements of the universe. QED
Note: it is perfectly possible that $\mr{WT}$ is in fact globally interpretable in $\mr{VSE}$, but I didn’t try.
Theorem 3: Each finite fragment $\mr{VSE}_k$ has a decidable consistent extension.
Corollary: Each finite fragment $\mr{WT}_k$ has a decidable consistent extension. Neither $\mr{VSE}$ nor $\mr{WT}$ interprets $Q$, or any finite essentially undecidable theory for that matter.
I will assume $k\ge2$. In order to prove Theorem 3, working in a usual set theory (e.g., ZFC), let $H_k$ denote the collection of all hereditarily $\le k$-element sets: the least family of sets such that
$$x\sset H_k\land|x|\le k\implies x\in H_k.$$
Note that $H_k\sset V_\omega$. Clearly,
$$(H_k,\in)\models\mr{VSE}_k,$$
thus Theorem 3 follows from
Theorem 4: $\mathrm{Th}(H_k,\in)$ is decidable.
This is proved in detail in [2]; let me sketch the basic argument.
Since any r.e. complete theory is decidable, it is enough to show that $\mathrm{Th}(H_k,\in)$ is recursively axiomatizable. In fact, I claim that it coincides with the theory $S_k$ axiomatized as follows:
$\mr{VSE}_k$ (i.e., extensionality, $V_0$ and $V_k$),
every set has at most $k$ elements,
there are no finite $\in$-cycles: i.e., the schema
$$\forall x_0,\dots,x_n\,\neg(x_0\in x_1\in\dots\in x_n\in x_0)$$
for $n\in\omega$.
Obviously $H_k\models S_k$, it thus suffices to show that $S_k$ is complete, i.e., that any two models of $S_k$ are elementarily equivalent. We will prove more generally a characterization of elementary equivalence of finite tuples in models of $S_k$.
Let $A,B$ be models of $S_k$, and $\bar a\in A$, $\bar b\in B$ finite tuples of the same length. We write $A,\bar a\equiv B,\bar b$ if $\bar a$ and $\bar b$ are elementarily equivalent.
We define levels of the transitive closure of $\bar a$ (as subsets of $A$):
$$\begin{align}
t^A_0(\bar a)&=\{\bar a\},\\
t^A_{n+1}(\bar a)&=t^A_n(\bar a)\cup\bigcup_{u\in t^A_n(\bar a)}u^A,\\
t^A_\infty(\bar a)&=\bigcup_{n\in\omega}t^A_n(\bar a),
\end{align}$$
where $u^A$ denotes the extension of $u\in A$ in $A$: $u^A=\{v\in A:v\in^A u\}$. Notice that each $t^A_n(\bar a)$ is finite: $|t^A_n(\bar a)|\le|\bar a|k^{n+1}$ or so. Also, each $t^A_n(\bar a)$ is definable (as a class) in $A$ from $\bar a$; the definition is uniform if $n$ and $|\bar a|$ are fixed.
Let us define
$$\begin{align}
A,\bar a\sim_n B,\bar b&\iff(t^A_n(\bar a),\in,\bar a)\simeq(t^B_n(\bar b),\in,\bar b),\\
A,\bar a\sim B,\bar b&\iff(t^A_\infty(\bar a),\in,\bar a)\simeq(t^B_\infty(\bar b),\in,\bar b).
\end{align}$$
Recall that elementarily equivalent finite structures are isomorphic. Thus, the finiteness and definability of $t^A_n(\bar a)$ implies
Claim 5: $A,\bar a\equiv B,\bar b\implies A,\bar a\sim_n B,\bar b$ for all $n\in\omega$.
Notice that $\bar a\sim_m\bar b$ implies $\bar a\sim_n\bar b$ for $n\le m$, as an isomorphism $t^A_m(\bar a)\simeq t^B_m(\bar b)$ must map $t^A_n(\bar a)$ to $t^B_n(\bar b)$. Thus, if we look at the set of all isomorphisms $f\colon t^A_n(\bar a)\simeq t^B_n(\bar b)$ for all $n\in\omega$, it forms a tree ordered by inclusion, and finiteness of the structures implies that the tree is finitely branching. Thus, if it is infinite, it has an infinite branch by König’s lemma, which is then an isomorphism $t^A_\infty(\bar a)\simeq t^B_\infty(\bar b)$. Thus,
Claim 6: $A,\bar a\sim B,\bar b\iff\forall n\in\omega\:A,\bar a\sim_n B,\bar b$.
Corollary 7: $A,\bar a\equiv B,\bar b\implies A,\bar a\sim B,\bar b$.
We intend to prove the converse
Claim 8: $A,\bar a\sim B,\bar b\implies A,\bar a\equiv B,\bar b$.
This finishes the proofs of Theorems 3 and 4, as it implies $A,\varnothing\equiv B,\varnothing$ for any $A,B\models S_k$.
By definition, it’s clear that $A,\bar a\sim_0 B,\bar b$ implies $\bar a$ and $\bar b$ have the same atomic diagram. Thus, by standard model-theoretic machinery, Claim 8 follows from the following back-and-forth property:
Claim 9: For every $n$, there exists $m$ such that whenever $A,\bar a\sim_m B,\bar b$ and $c\in A$, there exists $d\in B$ such that $A,\bar a,c\sim_n B,\bar b,d$.
Finally, using the fact that $\sim_n$ can be characterized by satisfaction of suitable formulas and the compactness theorem, it is enough to show
Claim 9’: If $A,\bar a\sim B,\bar b$, $c\in A$, and $n\in\omega$, there exists $d\in B$ such that $A,\bar a,c\sim_n B,\bar b,d$.
Proof: Let us fix an isomorphism $f\colon t^A_\infty(\bar a)\simeq t^B_\infty(\bar b)$. We need to extend $f$ to an isomorphism $g$ whose domain includes $t^A_n(c)$. For convenience, we will actually define $g$ as a map on $t^A_{n+1}(c)$, but it will not necessarily behave as an isomorphism on the extra points. Notice that $t^A_{n+1}(c)$ is a finite set, and $\in^A$ is acyclic, hence well founded, on it.
If there is $u\in t^A_{n+1}(c)\bez\dom(f)$ such that $u\sset\dom(f)$, we may extend $f$ right away so that $f(u)=\{f(x):x\in^A u\}^B$ (this exists in $B$, as it has at most $k$ elements). This maintains the salient property that $f$ is an isomorphism between two transitive closures of finite tuples. By repeating this construction as many times as necessary, we may assume without loss of generality that every $u\in t^A_{n+1}(c)\bez\dom(f)$ contains an element outside $\dom(f)$.
Now, let $\{u_i:i<m\}$ be an enumeration of $\{u\in t^A_{n+1}(c):u\nsubseteq t^A_{n+1}(c)\cup\dom(f)\}$. We pick suitable $\{v_i:i<m\}\sset B$ (to be determined below), and define $g\supseteq f$, $g(u_i)=v_i$. We then extend the definition to all $u\in t^A_{n+1}(c)$ inductively by $g(u)=\{g(x):x\in^A u\}^B$.
We need to make sure $g$ is injective. Now, if $u,u'\in t^A_n(c)\cup\dom(f)$ are distinct, there is $x$ in (say) $u\bez u'$; we have $x\in\dom(g)$, and $g(x)\in g(u)$, hence $g(x)\in g(u')$, i.e., $g(x)=g(x')$ for some $x'\ne x$, $x'\in u'$. By continuing down, we eventually arrive at $v_i=g(u)$ for some $u\ne u_i$. If $u\in\dom(f)$, this means $v_i=f(u)$. Otherwise we have $u_j=x_1\in\dots\in x_l\in u$ for some $j<m$, $0\le l\le n+1$, $x_1,\dots,x_l\in t^A_n(c)$. Thus, $v_j\in g(x_2)\in\dots\in g(u)=v_i$. (This can only happen for $j\ne i$.)
It follows that $g$ is injective if we choose $v_i$ to satisfy two conditions: (1) $v_i\notin\mathrm{im}(f)$ for any $i<m$, and (2) for any $i\ne j<m$, $v_i\notin t^B_{n+1}(v_j)$. It is easy to see that such $\{v_i:i<m\}$ exist: for example, we may put $w=\langle b_0,b_1,\dots\rangle$, and $v_i=\{w\}^{(n+2)i+1}$, where $\{w\}^0=w$, $\{w\}^{r+1}=\{\{w\}^r\}$.
It is clear from the definition that once $g$ is injective, we have $x\in u\iff g(x)\in g(u)$ for any $x\in\dom(g)$, $u\in\dom(f)\cup t^A_n(c)$. In particular, putting $d=g(c)$, the restriction of $g$ to $t^A_n(\bar a,c)$ is an isomorphism $t^A_n(\bar a,c)\simeq t^B_n(\bar b,d)$. QED
Using a more elaborate argument, one can show that the $m$ in Claim 9 can be bounded by $(k^{n+2}-1)/(k-1)+n+1$, which can be used to show that $S_k$ is decidable in iterated exponential time, matching known lower bounds for theories of pairing. See [2] for details.
Let me mention that Claim 8 also implies a quantifier elimination result for $S_k$. By compactness, for any formula $\phi(\bar x)$, there is $n$ such that the truth of $\phi$ is preserved by $\sim_n$. Thus, $\phi$ is equivalent to a disjunction of some of the (finitely many) formulas saying that $t_n(\bar x)$ looks such and such. This easily implies the following:
Corollary 10: In $S_k$, every formula is equivalent to a Boolean combination of bounded existential formulas. If we expand the language with the predicates $y=\varnothing$ and $y=\{x_1,\dots,x_k\}$, every formula is equivalent both to a bounded existential formula and to a bounded universal formula.
Reference:
[1] Albert Visser: Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), 299–326, doi: 10.1007/s00153-008-0087-1.
[2] Emil Jeřábek: The theory of hereditarily bounded sets, preprint, 2021, arXiv:2104.06932.
