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 → ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z ↔ ∀ w w ⊆ y → w ⊆ z → G ⁡ w ⊆ z
6 5 imbi1d ⊢ F = G → ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z ↔ ∀ w w ⊆ y → w ⊆ z → G ⁡ w ⊆ z → y ⊆ z
7 6 albidv ⊢ F = G → ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z ↔ ∀ z ∀ w w ⊆ y → w ⊆ z → G ⁡ w ⊆ z → y ⊆ z
8 7 abbidv ⊢ F = G → y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z = y | ∀ z ∀ w w ⊆ y → w ⊆ z → G ⁡ w ⊆ z → y ⊆ z
9 8 unieqd ⊢ F = G → ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z = ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → G ⁡ w ⊆ z → y ⊆ z
10 df-setrecs ⊢ setrecs ⁡ F = ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
11 df-setrecs ⊢ setrecs ⁡ G = ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → G ⁡ w ⊆ z → y ⊆ z
12 9 10 11 3eqtr4g ⊢ F = G → setrecs ⁡ F = setrecs ⁡ G