Theorem shiftstableeq2

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

	Ref	Expression
Assertion	shiftstableeq2	Could not format assertion : No typesetting found for |- ( F = G -> ( S ShiftStable F ) = ( S ShiftStable G ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		coeq2	$$⊢F=G\to S\circ F=S\circ G$$
2		id	$$⊢F=G\to F=G$$
3	1 2	ineq12d	$$⊢F=G\to \left(S\circ F\right)\cap F=\left(S\circ G\right)\cap G$$
4		df-shiftstable	Could not format ( S ShiftStable F ) = ( ( S o. F ) i^i F ) : No typesetting found for |- ( S ShiftStable F ) = ( ( S o. F ) i^i F ) with typecode |-
5		df-shiftstable	Could not format ( S ShiftStable G ) = ( ( S o. G ) i^i G ) : No typesetting found for |- ( S ShiftStable G ) = ( ( S o. G ) i^i G ) with typecode |-
6	3 4 5	3eqtr4g	Could not format ( F = G -> ( S ShiftStable F ) = ( S ShiftStable G ) ) : No typesetting found for |- ( F = G -> ( S ShiftStable F ) = ( S ShiftStable G ) ) with typecode |-