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 \|-

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 (S \circ F) \cap F = (S \circ G) \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 \|-

Metamath Proof Explorer