Metamath Proof Explorer

Theorem setrecseq

Description: Equality theorem for set recursion. (Contributed by Emmett Weisz, 17-Feb-2021)

Ref Expression
Assertion setrecseq ⊢F=G→setrecs⁡F=setrecs⁡G

Proof

Step Hyp Ref Expression
1 fveq1 ⊢F=G→F⁡w=G⁡w
2 1 sseq1d ⊢F=G→F⁡w⊆z↔G⁡w⊆z
3 2 imbi2d ⊢F=G→w⊆z→F⁡w⊆z↔w⊆z→G⁡w⊆z
4 3 imbi2d ⊢F=G→w⊆y→w⊆z→F⁡w⊆z↔w⊆y→w⊆z→G⁡w⊆z
5 4 albidv ⊢F=G→∀ww⊆y→w⊆z→F⁡w⊆z↔∀ww⊆y→w⊆z→G⁡w⊆z
6 5 imbi1d ⊢F=G→∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z↔∀ww⊆y→w⊆z→G⁡w⊆z→y⊆z
7 6 albidv ⊢F=G→∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z↔∀z∀ww⊆y→w⊆z→G⁡w⊆z→y⊆z
8 7 abbidv ⊢F=G→y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z=y|∀z∀ww⊆y→w⊆z→G⁡w⊆z→y⊆z
9 8 unieqd ⊢F=G→⋃y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z=⋃y|∀z∀ww⊆y→w⊆z→G⁡w⊆z→y⊆z
10 df-setrecs ⊢setrecs⁡F=⋃y|∀z∀ww⊆y→w⊆z→F⁡w⊆z→y⊆z
11 df-setrecs ⊢setrecs⁡G=⋃y|∀z∀ww⊆y→w⊆z→G⁡w⊆z→y⊆z
12 9 10 11 3eqtr4g ⊢F=G→setrecs⁡F=setrecs⁡G