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

Theorem isoeq1 7309
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 6818 . . 3 (𝐻 = 𝐺 → (𝐻:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
2 fveq1 6887 . . . . . 6 (𝐻 = 𝐺 → (𝐻𝑥) = (𝐺𝑥))
3 fveq1 6887 . . . . . 6 (𝐻 = 𝐺 → (𝐻𝑦) = (𝐺𝑦))
42, 3breq12d 5160 . . . . 5 (𝐻 = 𝐺 → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐺𝑥)𝑆(𝐺𝑦)))
54bibi2d 343 . . . 4 (𝐻 = 𝐺 → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
652ralbidv 3219 . . 3 (𝐻 = 𝐺 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
71, 6anbi12d 632 . 2 (𝐻 = 𝐺 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐺:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦)))))
8 df-isom 6549 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
9 df-isom 6549 . 2 (𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐺:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
107, 8, 93bitr4g 314 1 (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wral 3062   class class class wbr 5147  1-1-ontowf1o 6539  cfv 6540   Isom wiso 6541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549
This theorem is referenced by:  isores1  7326  wemoiso  7955  wemoiso2  7956  ordiso  9507  oieu  9530  finnisoeu  10104  iunfictbso  10105  infrenegsup  12193  ltweuz  13922  fz1isolem  14418  isercolllem2  15608  isercoll  15610  dvgt0lem2  25502  efcvx  25943  relogiso  26088  logccv  26153  erdszelem1  34120  erdsze  34131  erdsze2lem2  34133  isoeq145d  42103  fzisoeu  43945  fourierdlem36  44794  fourierdlem96  44853  fourierdlem97  44854  fourierdlem98  44855  fourierdlem99  44856  fourierdlem105  44862  fourierdlem106  44863  fourierdlem108  44865  fourierdlem110  44867  fourierdlem112  44869  fourierdlem113  44870  fourierdlem115  44872  rrx2plordisom  47311
  Copyright terms: Public domain W3C validator