Metamath Proof Explorer

Theorem r10

Description: Value of the cumulative hierarchy of sets function at (/) . Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by NM, 2-Sep-2003) (Revised by Mario Carneiro, 10-Sep-2013)

		Ref	Expression
	Assertion	r10	$⊢ R_{1} (\emptyset) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-r1	$⊢ R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$
2	1	fveq1i	$⊢ R_{1} (\emptyset) = rec ((x \in V ⟼ 𝒫 x), \emptyset) (\emptyset)$
3		0ex	$⊢ \emptyset \in V$
4	3	rdg0	$⊢ rec ((x \in V ⟼ 𝒫 x), \emptyset) (\emptyset) = \emptyset$
5	2 4	eqtri	$⊢ R_{1} (\emptyset) = \emptyset$