Theorem isoeq4 6201

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 5791	. . 3 |- ( A = C -> ( H : A -1-1-onto-> B <-> H : C -1-1-onto-> B ) )
2		raleq 3004	. . . 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 3012	. . 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 709	. 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 5578	. 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 5578	. 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 367   = wceq 1405   A.wral 2754   class class class wbr 4395   -1-1-onto->wf1o 5568   ` cfv 5569   Isom wiso 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-isom 5578

This theorem is referenced by:  oieu  7998  oiid  8000  finnisoeu  8526  iunfictbso  8527  fz1isolem  12559  isercolllem3  13638  summolem2a  13686  prodmolem2a  13893  erdszelem1  29488  erdsze  29499  erdsze2lem1  29500  erdsze2lem2  29501  fzisoeu  36869  fourierdlem36  37293  fourierdlem112  37369  fourierdlem113  37370