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

Theorem isoeq1 7065
Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
Assertion
Ref Expression
isoeq1 (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))

Proof of Theorem isoeq1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq1 6600 . . 3 (𝐻 = 𝐺 → (𝐻:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
2 fveq1 6665 . . . . . 6 (𝐻 = 𝐺 → (𝐻𝑥) = (𝐺𝑥))
3 fveq1 6665 . . . . . 6 (𝐻 = 𝐺 → (𝐻𝑦) = (𝐺𝑦))
42, 3breq12d 5075 . . . . 5 (𝐻 = 𝐺 → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐺𝑥)𝑆(𝐺𝑦)))
54bibi2d 344 . . . 4 (𝐻 = 𝐺 → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
652ralbidv 3203 . . 3 (𝐻 = 𝐺 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
71, 6anbi12d 630 . 2 (𝐻 = 𝐺 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐺:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦)))))
8 df-isom 6360 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
9 df-isom 6360 . 2 (𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐺:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
107, 8, 93bitr4g 315 1 (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wral 3142   class class class wbr 5062  1-1-ontowf1o 6350  cfv 6351   Isom wiso 6352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360
This theorem is referenced by:  isores1  7082  wemoiso  7668  wemoiso2  7669  ordiso  8972  oieu  8995  finnisoeu  9531  iunfictbso  9532  infrenegsup  11616  ltweuz  13322  fz1isolem  13812  isercolllem2  15015  isercoll  15017  dvgt0lem2  24515  efcvx  24952  relogiso  25094  logccv  25159  erdszelem1  32322  erdsze  32333  erdsze2lem2  32335  fzisoeu  41428  fourierdlem36  42290  fourierdlem96  42349  fourierdlem97  42350  fourierdlem98  42351  fourierdlem99  42352  fourierdlem105  42358  fourierdlem106  42359  fourierdlem108  42361  fourierdlem110  42363  fourierdlem112  42365  fourierdlem113  42366  fourierdlem115  42368  rrx2plordisom  44538
  Copyright terms: Public domain W3C validator