Theorem isoeq1 6203

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

Assertion

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

Proof of Theorem isoeq1

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

Step	Hyp	Ref	Expression
1		f1oeq1 5807	. . 3 |- ( H = G -> ( H : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )
2		fveq1 5865	. . . . . 6 |- ( H = G -> ( H ` x ) = ( G ` x ) )
3		fveq1 5865	. . . . . 6 |- ( H = G -> ( H ` y ) = ( G ` y ) )
4	2, 3	breq12d 4460	. . . . 5 |- ( H = G -> ( ( H ` x ) S ( H ` y ) <-> ( G ` x ) S ( G ` y ) ) )
5	4	bibi2d 318	. . . 4 |- ( H = G -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( x R y <-> ( G ` x ) S ( G ` y ) ) ) )
6	5	2ralbidv 2908	. . 3 |- ( 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 710	. 2 |- ( 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 5597	. 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 ) ) ) )
9		df-isom 5597	. 2 |- ( 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 288	1 |- ( H = G -> ( H Isom R , S ( A , B ) <-> G Isom R , S ( A , B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   A.wral 2814   class class class wbr 4447   -1-1-onto->wf1o 5587   ` cfv 5588   Isom wiso 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597

This theorem is referenced by:  isores1  6218  wemoiso  6769  wemoiso2  6770  ordiso  7941  oieu  7964  finnisoeu  8494  iunfictbso  8495  infmsup  10521  ltweuz  12040  fz1isolem  12476  isercolllem2  13451  isercoll  13453  dvgt0lem2  22167  efcvx  22606  relogiso  22738  logccv  22800  erdszelem1  28303  erdsze  28314  erdsze2lem2  28316  fzisoeu  31105  fourierdlem36  31471  fourierdlem54  31489  fourierdlem96  31531  fourierdlem97  31532  fourierdlem98  31533  fourierdlem99  31534  fourierdlem105  31540  fourierdlem106  31541  fourierdlem108  31543  fourierdlem110  31545  fourierdlem112  31547  fourierdlem113  31548  fourierdlem115  31550