Theorem isoeq5

Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004)

	Ref	Expression
Assertion	isoeq5	$$⊢B=C\to \left(H{Isom}_{R,S}\left(A,B\right)\leftrightarrow H{Isom}_{R,S}\left(A,C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1oeq3	$$⊢B=C\to \left(H:A\underset{1-1\; onto}{⟶}B\leftrightarrow H:A\underset{1-1\; onto}{⟶}C\right)$$
2	1	anbi1d	$$⊢B=C\to \left(\left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}C\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)\right)$$
3		df-isom	$$⊢H{Isom}_{R,S}\left(A,B\right)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)$$
4		df-isom	$$⊢H{Isom}_{R,S}\left(A,C\right)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}C\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)$$
5	2 3 4	3bitr4g	$$⊢B=C\to \left(H{Isom}_{R,S}\left(A,B\right)\leftrightarrow H{Isom}_{R,S}\left(A,C\right)\right)$$