![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > isof1o | GIF version |
Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
Ref | Expression |
---|---|
isof1o | ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-isom 5244 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wral 2468 class class class wbr 4018 –1-1-onto→wf1o 5234 ‘cfv 5235 Isom wiso 5236 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-isom 5244 |
This theorem is referenced by: isocnv2 5834 isores1 5836 isoini 5840 isoini2 5841 isoselem 5842 isose 5843 isopolem 5844 isosolem 5846 smoiso 6327 isotilem 7035 supisolem 7037 supisoex 7038 supisoti 7039 ordiso2 7064 leisorel 10849 zfz1isolemiso 10851 seq3coll 10854 summodclem2a 11421 prodmodclem2a 11616 |
Copyright terms: Public domain | W3C validator |