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 𝑅1

Proof

Step	Hyp	Ref	Expression
1		rdgfun	⊢ Fun rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
2		df-r1	⊢ 𝑅1 = rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
3	2	funeqi	⊢ ( Fun 𝑅1 ↔ Fun rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) )
4	1 3	mpbir	⊢ Fun 𝑅1