Theorem isoeq5

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

	Ref	Expression
Assertion	isoeq5	|- ( B = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( A , C ) ) )

Proof

Step	Hyp	Ref	Expression
1		f1oeq3	|- ( B = C -> ( H : A -1-1-onto-> B <-> H : A -1-1-onto-> C ) )
2	1	anbi1d	|- ( B = C -> ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) <-> ( H : A -1-1-onto-> C /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) )
3		df-isom	|- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
4		df-isom	|- ( H Isom R , S ( A , C ) <-> ( H : A -1-1-onto-> C /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
5	2 3 4	3bitr4g	|- ( B = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( A , C ) ) )