Theorem isoeq2

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

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

Proof

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