|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > isoeq5 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) | 
| Ref | Expression | 
|---|---|
| isoeq5 | ⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | f1oeq3 6837 | . . 3 ⊢ (𝐵 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐴–1-1-onto→𝐶)) | |
| 2 | 1 | anbi1d 631 | . 2 ⊢ (𝐵 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))) | 
| 3 | df-isom 6569 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
| 4 | df-isom 6569 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∀wral 3060 class class class wbr 5142 –1-1-onto→wf1o 6559 ‘cfv 6560 Isom wiso 6561 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-ss 3967 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-isom 6569 | 
| This theorem is referenced by: isores3 7356 ordiso 9557 ordtypelem9 9567 ordtypelem10 9568 oiid 9582 iunfictbso 10155 ltweuz 14003 fz1isolem 14501 dvgt0lem2 26043 erdszelem1 35197 erdsze 35208 erdsze2lem1 35209 erdsze2lem2 35210 isoeq145d 43437 alephiso3 43577 fourierdlem50 46176 fourierdlem89 46215 fourierdlem90 46216 fourierdlem91 46217 fourierdlem96 46222 fourierdlem97 46223 fourierdlem98 46224 fourierdlem99 46225 fourierdlem100 46226 fourierdlem108 46234 fourierdlem110 46236 fourierdlem112 46238 fourierdlem113 46239 | 
| Copyright terms: Public domain | W3C validator |