Theorem setrecseq

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

	Ref	Expression
Assertion	setrecseq	⊢ ( 𝐹 = 𝐺 → setrecs ( 𝐹 ) = setrecs ( 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
2	1	sseq1d	⊢ ( 𝐹 = 𝐺 → ( ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ↔ ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) )
3	2	imbi2d	⊢ ( 𝐹 = 𝐺 → ( ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ↔ ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) )
4	3	imbi2d	⊢ ( 𝐹 = 𝐺 → ( ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) )
5	4	albidv	⊢ ( 𝐹 = 𝐺 → ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) ) )
6	5	imbi1d	⊢ ( 𝐹 = 𝐺 → ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ) )
7	6	albidv	⊢ ( 𝐹 = 𝐺 → ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ) )
8	7	abbidv	⊢ ( 𝐹 = 𝐺 → { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } )
9	8	unieqd	⊢ ( 𝐹 = 𝐺 → ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } )
10		df-setrecs	⊢ setrecs ( 𝐹 ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
11		df-setrecs	⊢ setrecs ( 𝐺 ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐺 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
12	9 10 11	3eqtr4g	⊢ ( 𝐹 = 𝐺 → setrecs ( 𝐹 ) = setrecs ( 𝐺 ) )