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

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

Proof of Theorem isoeq5
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq3 6597 . . 3 (𝐵 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐴1-1-onto𝐶))
21anbi1d 632 . 2 (𝐵 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
3 df-isom 6349 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
4 df-isom 6349 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
52, 3, 43bitr4g 317 1 (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∀wral 3070   class class class wbr 5036  –1-1-onto→wf1o 6339  ‘cfv 6340   Isom wiso 6341 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-isom 6349 This theorem is referenced by:  isores3  7088  ordiso  9026  ordtypelem9  9036  ordtypelem10  9037  oiid  9051  iunfictbso  9587  ltweuz  13391  fz1isolem  13884  dvgt0lem2  24715  erdszelem1  32681  erdsze  32692  erdsze2lem1  32693  erdsze2lem2  32694  alephiso3  40666  fourierdlem50  43199  fourierdlem89  43238  fourierdlem90  43239  fourierdlem91  43240  fourierdlem96  43245  fourierdlem97  43246  fourierdlem98  43247  fourierdlem99  43248  fourierdlem100  43249  fourierdlem108  43257  fourierdlem110  43259  fourierdlem112  43261  fourierdlem113  43262
 Copyright terms: Public domain W3C validator