Metamath Proof Explorer

Theorem shiftstableeq2

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

Ref Expression
Assertion shiftstableeq2 
|- ( F = G -> ( S ShiftStable F ) = ( S ShiftStable G ) )

Proof

Step Hyp Ref Expression
1 coeq2 
 |-  ( F = G -> ( S o. F ) = ( S o. G ) )
2 id 
 |-  ( F = G -> F = G )
3 1 2 ineq12d 
 |-  ( F = G -> ( ( S o. F ) i^i F ) = ( ( S o. G ) i^i G ) )
4 df-shiftstable 
 |-  ( S ShiftStable F ) = ( ( S o. F ) i^i F )
5 df-shiftstable 
 |-  ( S ShiftStable G ) = ( ( S o. G ) i^i G )
6 3 4 5 3eqtr4g 
 |-  ( F = G -> ( S ShiftStable F ) = ( S ShiftStable G ) )