This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rdg0g

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

Ref Expression
Assertion rdg0g ⊢ A ∈ C → rec ⁡ F A ⁡ ∅ = A

Proof

Step Hyp Ref Expression
1 rdgeq2 ⊢ x = A → rec ⁡ F x = rec ⁡ F A
2 1 fveq1d ⊢ x = A → rec ⁡ F x ⁡ ∅ = rec ⁡ F A ⁡ ∅
3 id ⊢ x = A → x = A
4 2 3 eqeq12d ⊢ x = A → rec ⁡ F x ⁡ ∅ = x ↔ rec ⁡ F A ⁡ ∅ = A
5 vex ⊢ x ∈ V
6 5 rdg0 ⊢ rec ⁡ F x ⁡ ∅ = x
7 4 6 vtoclg ⊢ A ∈ C → rec ⁡ F A ⁡ ∅ = A