Metamath Proof Explorer

Theorem r1fun

Description: The cumulative hierarchy of sets function is a function. (Contributed by Mario Carneiro, 16-Nov-2014) Extract this statement from its conjunction with r1dmlim . (Revised by BJ, 27-Sep-2026)

		Ref	Expression
	Assertion	r1fun	$⊢ Fun R_{1}$

Proof

Step	Hyp	Ref	Expression
1		rdgfun	$⊢ Fun rec ((x \in V ⟼ 𝒫 x), \emptyset)$
2		df-r1	$⊢ R_{1} = rec ((x \in V ⟼ 𝒫 x), \emptyset)$
3	2	funeqi	$⊢ Fun R_{1} \leftrightarrow Fun rec ((x \in V ⟼ 𝒫 x), \emptyset)$
4	1 3	mpbir	$⊢ Fun R_{1}$