MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isoeq1 Structured version   Unicode version

Theorem isoeq1 6216
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.
StepHypRef Expression
1 f1oeq1 5813 . . 3  |-  ( H  =  G  ->  ( H : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )
2 fveq1 5871 . . . . . 6  |-  ( H  =  G  ->  ( H `  x )  =  ( G `  x ) )
3 fveq1 5871 . . . . . 6  |-  ( H  =  G  ->  ( H `  y )  =  ( G `  y ) )
42, 3breq12d 4430 . . . . 5  |-  ( H  =  G  ->  (
( H `  x
) S ( H `
 y )  <->  ( G `  x ) S ( G `  y ) ) )
54bibi2d 319 . . . 4  |-  ( H  =  G  ->  (
( x R y  <-> 
( H `  x
) S ( H `
 y ) )  <-> 
( x R y  <-> 
( G `  x
) S ( G `
 y ) ) ) )
652ralbidv 2867 . . 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 ) ) ) )
71, 6anbi12d 715 . 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 5601 . 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 5601 . 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 ) ) ) )
107, 8, 93bitr4g 291 1  |-  ( H  =  G  ->  ( H  Isom  R ,  S  ( A ,  B )  <-> 
G  Isom  R ,  S  ( A ,  B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   A.wral 2773   class class class wbr 4417   -1-1-onto->wf1o 5591   ` cfv 5592    Isom wiso 5593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-isom 5601
This theorem is referenced by:  isores1  6231  wemoiso  6783  wemoiso2  6784  ordiso  8022  oieu  8045  finnisoeu  8533  iunfictbso  8534  infrenegsup  10580  infmsupOLD  10581  ltweuz  12161  fz1isolem  12608  isercolllem2  13696  isercoll  13698  dvgt0lem2  22829  efcvx  23266  relogiso  23409  logccv  23470  erdszelem1  29699  erdsze  29710  erdsze2lem2  29712  fzisoeu  37131  fourierdlem36  37578  fourierdlem96  37638  fourierdlem97  37639  fourierdlem98  37640  fourierdlem99  37641  fourierdlem105  37647  fourierdlem106  37648  fourierdlem108  37650  fourierdlem110  37652  fourierdlem112  37654  fourierdlem113  37655  fourierdlem115  37657
  Copyright terms: Public domain W3C validator