Theorem isoeq1

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

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

Proof

Step	Hyp	Ref	Expression
1		f1oeq1	|- ( H = G -> ( H : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )
2		fveq1	|- ( H = G -> ( H ` x ) = ( G ` x ) )
3		fveq1	|- ( H = G -> ( H ` y ) = ( G ` y ) )
4	2 3	breq12d	|- ( H = G -> ( ( H ` x ) S ( H ` y ) <-> ( G ` x ) S ( G ` y ) ) )
5	4	bibi2d	|- ( H = G -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( x R y <-> ( G ` x ) S ( G ` y ) ) ) )
6	5	2ralbidv	|- ( H = G -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. x e. A A. y e. A ( x R y <-> ( G ` x ) S ( G ` y ) ) ) )
7	1 6	anbi12d	|- ( H = G -> ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) <-> ( G : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( G ` x ) S ( G ` y ) ) ) ) )
8		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 ) ) ) )
9		df-isom	|- ( G Isom R , S ( A , B ) <-> ( G : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( G ` x ) S ( G ` y ) ) ) )
10	7 8 9	3bitr4g	|- ( H = G -> ( H Isom R , S ( A , B ) <-> G Isom R , S ( A , B ) ) )