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 ) C_ z <-> ( G ` w ) C_ z ) )
3 2 imbi2d 
 |-  ( F = G -> ( ( w C_ z -> ( F ` w ) C_ z ) <-> ( w C_ z -> ( G ` w ) C_ z ) ) )
4 3 imbi2d 
 |-  ( F = G -> ( ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) <-> ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) ) )
5 4 albidv 
 |-  ( F = G -> ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) <-> A. w ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) ) )
6 5 imbi1d 
 |-  ( F = G -> ( ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) <-> ( A. w ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) -> y C_ z ) ) )
7 6 albidv 
 |-  ( F = G -> ( A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) <-> A. z ( A. w ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) -> y C_ z ) ) )
8 7 abbidv 
 |-  ( F = G -> { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) -> y C_ z ) } )
9 8 unieqd 
 |-  ( F = G -> U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) -> y C_ z ) } )
10 df-setrecs 
 |-  setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
11 df-setrecs 
 |-  setrecs ( G ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( G ` w ) C_ z ) ) -> y C_ z ) }
12 9 10 11 3eqtr4g 
 |-  ( F = G -> setrecs ( F ) = setrecs ( G ) )