Theorem rdg0g

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

	Ref	Expression
Assertion	rdg0g	$$⊢A\in C\to \mathrm{rec}\left(F,A\right)\left(\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		rdgeq2	$$⊢x=A\to \mathrm{rec}\left(F,x\right)=\mathrm{rec}\left(F,A\right)$$
2	1	fveq1d	$$⊢x=A\to \mathrm{rec}\left(F,x\right)\left(\varnothing \right)=\mathrm{rec}\left(F,A\right)\left(\varnothing \right)$$
3		id	$$⊢x=A\to x=A$$
4	2 3	eqeq12d	$$⊢x=A\to \left(\mathrm{rec}\left(F,x\right)\left(\varnothing \right)=x\leftrightarrow \mathrm{rec}\left(F,A\right)\left(\varnothing \right)=A\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	rdg0	$$⊢\mathrm{rec}\left(F,x\right)\left(\varnothing \right)=x$$
7	4 6	vtoclg	$$⊢A\in C\to \mathrm{rec}\left(F,A\right)\left(\varnothing \right)=A$$