Theorem unir1regs

Description: The cumulative hierarchy of sets covers the universe. This version of unir1 replaces setind with setindregs . (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	unir1regs	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		setindregs	$$⊢\forall x\left(x\subseteq \bigcup R_1\left[\mathrm{On}\right]\to x\in \bigcup R_1\left[\mathrm{On}\right]\right)\to \bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	r1elss	$$⊢x\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow x\subseteq \bigcup R_1\left[\mathrm{On}\right]$$
4	3	biimpri	$$⊢x\subseteq \bigcup R_1\left[\mathrm{On}\right]\to x\in \bigcup R_1\left[\mathrm{On}\right]$$
5	1 4	mpg	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$