Theorem isoeq3

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

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

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢S=T\to \left(H\left(x\right)SH\left(y\right)\leftrightarrow H\left(x\right)TH\left(y\right)\right)$$
2	1	bibi2d	$$⊢S=T\to \left(\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\leftrightarrow \left(xRy\leftrightarrow H\left(x\right)TH\left(y\right)\right)\right)$$
3	2	2ralbidv	$$⊢S=T\to \left(\forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\leftrightarrow \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)TH\left(y\right)\right)\right)$$
4	3	anbi2d	$$⊢S=T\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}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)TH\left(y\right)\right)\right)\right)$$
5		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)$$
6		df-isom	$$⊢H{Isom}_{R,T}\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)TH\left(y\right)\right)\right)$$
7	4 5 6	3bitr4g	$$⊢S=T\to \left(H{Isom}_{R,S}\left(A,B\right)\leftrightarrow H{Isom}_{R,T}\left(A,B\right)\right)$$