Theorem jech9.3

Description: Every set belongs to some stage of the cumulative hierarchy of sets, expressed using an indexed union. Lemma 9.3 of Jech p. 71. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 8-Jun-2013) (Proof shortened by BJ, 29-Sep-2026)

	Ref	Expression
Assertion	jech9.3	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		r1fun	$$⊢\mathrm{Fun}{R}_1$$
2		funiunfv	$$⊢\mathrm{Fun}{R}_1\to \bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]$$
3	1 2	ax-mp	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]$$
4		unir1	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
5	3 4	eqtri	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\mathrm{V}$$