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 6042 | . . 3 ⊢ (𝐵 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐴–1-1-onto→𝐶)) | |
2 | 1 | anbi1d 737 | . 2 ⊢ (𝐵 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))) |
3 | df-isom 5813 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
4 | df-isom 5813 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
5 | 2, 3, 4 | 3bitr4g 302 | 1 ⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∀wral 2896 class class class wbr 4583 –1-1-onto→wf1o 5803 ‘cfv 5804 Isom wiso 5805 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-isom 5813 |
This theorem is referenced by: isores3 6485 ordiso 8304 ordtypelem9 8314 ordtypelem10 8315 oiid 8329 iunfictbso 8820 ltweuz 12622 fz1isolem 13102 dvgt0lem2 23570 erdszelem1 30427 erdsze 30438 erdsze2lem1 30439 erdsze2lem2 30440 fourierdlem50 39049 fourierdlem89 39088 fourierdlem90 39089 fourierdlem91 39090 fourierdlem96 39095 fourierdlem97 39096 fourierdlem98 39097 fourierdlem99 39098 fourierdlem100 39099 fourierdlem108 39107 fourierdlem110 39109 fourierdlem112 39111 fourierdlem113 39112 |
Copyright terms: Public domain | W3C validator |