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⁡FA=rec⁡FB

Proof

Step Hyp Ref Expression
1 ifeq1 ⊢A=B→ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=ifg=∅BifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
2 1 mpteq2dv ⊢A=B→g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V⟼ifg=∅BifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
3 recseq ⊢g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=g∈V⟼ifg=∅BifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g→recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=recs⁡g∈V⟼ifg=∅BifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
4 2 3 syl ⊢A=B→recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g=recs⁡g∈V⟼ifg=∅BifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
5 df-rdg ⊢rec⁡FA=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
6 df-rdg ⊢rec⁡FB=recs⁡g∈V⟼ifg=∅BifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
7 4 5 6 3eqtr4g ⊢A=B→rec⁡FA=rec⁡FB