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	⊢ ( 𝑅1 ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-r1	⊢ 𝑅1 = rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ )
2	1	fveq1i	⊢ ( 𝑅1 ‘ ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ ∅ )
3		0ex	⊢ ∅ ∈ V
4	3	rdg0	⊢ ( rec ( ( 𝑥 ∈ V ↦ 𝒫 𝑥 ) , ∅ ) ‘ ∅ ) = ∅
5	2 4	eqtri	⊢ ( 𝑅1 ‘ ∅ ) = ∅