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	|- U. ( R1 " On ) = _V

Proof

Step	Hyp	Ref	Expression
1		setindregs	|- ( A. x ( x C_ U. ( R1 " On ) -> x e. U. ( R1 " On ) ) -> U. ( R1 " On ) = _V )
2		vex	|- x e. _V
3	2	r1elss	|- ( x e. U. ( R1 " On ) <-> x C_ U. ( R1 " On ) )
4	3	biimpri	|- ( x C_ U. ( R1 " On ) -> x e. U. ( R1 " On ) )
5	1 4	mpg	|- U. ( R1 " On ) = _V