Theorem shiftstableeq2

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

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

Proof

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