Theorem resisoeq45d

Description: Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025)

	Ref	Expression
Hypotheses	resisoeq45.4	$$⊢\phi \to A=C$$
	resisoeq45.5	$$⊢\phi \to B=D$$
Assertion	resisoeq45d	$$⊢\phi \to \left(\left({F\upharpoonright }_A\right){Isom}_{R,S}\left(A,B\right)\leftrightarrow \left({F\upharpoonright }_C\right){Isom}_{R,S}\left(C,D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		resisoeq45.4	$$⊢\phi \to A=C$$
2		resisoeq45.5	$$⊢\phi \to B=D$$
3	1	reseq2d	$$⊢\phi \to {F\upharpoonright }_A={F\upharpoonright }_C$$
4	3 1 2	isoeq145d	$$⊢\phi \to \left(\left({F\upharpoonright }_A\right){Isom}_{R,S}\left(A,B\right)\leftrightarrow \left({F\upharpoonright }_C\right){Isom}_{R,S}\left(C,D\right)\right)$$