Theorem negslem1

Description: An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024)

	Ref	Expression
Assertion	negslem1	$$⊢A=B\to \left(\left({F\upharpoonright }_A\right){Isom}_{R,R^{-1}}\left(A,A\right)\leftrightarrow \left({F\upharpoonright }_B\right){Isom}_{R,R^{-1}}\left(B,B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A=B\to A=B$$
2	1 1	resisoeq45d	$$⊢A=B\to \left(\left({F\upharpoonright }_A\right){Isom}_{R,R^{-1}}\left(A,A\right)\leftrightarrow \left({F\upharpoonright }_B\right){Isom}_{R,R^{-1}}\left(B,B\right)\right)$$