Theorem shiftstableeq2 38653

Description: Equality theorem for shift-stability of two classes. (Contributed by Peter Mazsa, 19-Feb-2026.)

Assertion

Ref	Expression
shiftstableeq2	⊢ (𝐹 = 𝐺 → (𝑆 ShiftStable 𝐹) = (𝑆 ShiftStable 𝐺))

Proof of Theorem shiftstableeq2

Step	Hyp	Ref	Expression
1		coeq2 5806	. . 3 ⊢ (𝐹 = 𝐺 → (𝑆 ∘ 𝐹) = (𝑆 ∘ 𝐺))
2		id 22	. . 3 ⊢ (𝐹 = 𝐺 → 𝐹 = 𝐺)
3	1, 2	ineq12d 4172	. 2 ⊢ (𝐹 = 𝐺 → ((𝑆 ∘ 𝐹) ∩ 𝐹) = ((𝑆 ∘ 𝐺) ∩ 𝐺))
4		df-shiftstable 38652	. 2 ⊢ (𝑆 ShiftStable 𝐹) = ((𝑆 ∘ 𝐹) ∩ 𝐹)
5		df-shiftstable 38652	. 2 ⊢ (𝑆 ShiftStable 𝐺) = ((𝑆 ∘ 𝐺) ∩ 𝐺)
6	3, 4, 5	3eqtr4g 2795	1 ⊢ (𝐹 = 𝐺 → (𝑆 ShiftStable 𝐹) = (𝑆 ShiftStable 𝐺))

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3899   ∘ ccom 5627   ShiftStable cshiftstable 38352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-in 3907  df-ss 3917  df-br 5098  df-opab 5160  df-co 5632  df-shiftstable 38652

This theorem is referenced by:  dfpet2parts2  39143  pets2eq  39147