Theorem isoeq4 6197

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

Assertion

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

Proof of Theorem isoeq4

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1oeq2 5799	. . 3 |- ( A = C -> ( H : A -1-1-onto-> B <-> H : C -1-1-onto-> B ) )
2		raleq 3051	. . . 4 |- ( A = C -> ( A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
3	2	raleqbi1dv 3059	. . 3 |- ( A = C -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
4	1, 3	anbi12d 710	. 2 |- ( A = C -> ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) <-> ( H : C -1-1-onto-> B /\ A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) )
5		df-isom 5588	. 2 |- ( 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 ) ) ) )
6		df-isom 5588	. 2 |- ( H Isom R , S ( C , B ) <-> ( H : C -1-1-onto-> B /\ A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
7	4, 5, 6	3bitr4g 288	1 |- ( A = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( C , B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1374   A.wral 2807   class class class wbr 4440   -1-1-onto->wf1o 5578   ` cfv 5579   Isom wiso 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-isom 5588

This theorem is referenced by:  oieu  7953  oiid  7955  finnisoeu  8483  iunfictbso  8484  fz1isolem  12463  isercolllem3  13438  summolem2a  13486  erdszelem1  28125  erdsze  28136  erdsze2lem1  28137  erdsze2lem2  28138  prodmolem2a  28493  fzisoeu  30896  fourierdlem36  31262  fourierdlem54  31280  fourierdlem112  31338  fourierdlem113  31339