Theorem rdg0g

Description: The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995)

	Ref	Expression
Assertion	rdg0g	⊢ ( 𝐴 ∈ 𝐶 → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rdgeq2	⊢ ( 𝑥 = 𝐴 → rec ( 𝐹 , 𝑥 ) = rec ( 𝐹 , 𝐴 ) )
2	1	fveq1d	⊢ ( 𝑥 = 𝐴 → ( rec ( 𝐹 , 𝑥 ) ‘ ∅ ) = ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) )
3		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( rec ( 𝐹 , 𝑥 ) ‘ ∅ ) = 𝑥 ↔ ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 ) )
5		vex	⊢ 𝑥 ∈ V
6	5	rdg0	⊢ ( rec ( 𝐹 , 𝑥 ) ‘ ∅ ) = 𝑥
7	4 6	vtoclg	⊢ ( 𝐴 ∈ 𝐶 → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 )