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

Theorem isoeq5 7267
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 6775 . . 3 (𝐵 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐴1-1-onto𝐶))
21anbi1d 631 . 2 (𝐵 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
3 df-isom 6506 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
4 df-isom 6506 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
52, 3, 43bitr4g 314 1 (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wral 3061   class class class wbr 5106  1-1-ontowf1o 6496  cfv 6497   Isom wiso 6498
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-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-isom 6506
This theorem is referenced by:  isores3  7281  ordiso  9457  ordtypelem9  9467  ordtypelem10  9468  oiid  9482  iunfictbso  10055  ltweuz  13872  fz1isolem  14366  dvgt0lem2  25383  erdszelem1  33842  erdsze  33853  erdsze2lem1  33854  erdsze2lem2  33855  isoeq145d  41779  alephiso3  41919  fourierdlem50  44483  fourierdlem89  44522  fourierdlem90  44523  fourierdlem91  44524  fourierdlem96  44529  fourierdlem97  44530  fourierdlem98  44531  fourierdlem99  44532  fourierdlem100  44533  fourierdlem108  44541  fourierdlem110  44543  fourierdlem112  44545  fourierdlem113  44546
  Copyright terms: Public domain W3C validator