Metamath Proof Explorer

Theorem rdgeq2

Description: Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion rdgeq2 ⊢ A = B → rec ⁡ F A = rec ⁡ F B

Proof

Step Hyp Ref Expression
1 ifeq1 ⊢ A = B → if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if g = ∅ B if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
2 1 mpteq2dv ⊢ A = B → g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ B if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
3 recseq ⊢ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ B if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g → recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ B if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
4 2 3 syl ⊢ A = B → recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ B if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
5 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
6 df-rdg ⊢ rec ⁡ F B = recs ⁡ g ∈ V ⟼ if g = ∅ B if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
7 4 5 6 3eqtr4g ⊢ A = B → rec ⁡ F A = rec ⁡ F B