Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > isof1o | Unicode version |
Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
Ref | Expression |
---|---|
isof1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-isom 5102 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wral 2393 class class class wbr 3899 wf1o 5092 cfv 5093 wiso 5094 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-isom 5102 |
This theorem is referenced by: isocnv2 5681 isores1 5683 isoini 5687 isoini2 5688 isoselem 5689 isose 5690 isopolem 5691 isosolem 5693 smoiso 6167 isotilem 6861 supisolem 6863 supisoex 6864 supisoti 6865 ordiso2 6888 leisorel 10548 zfz1isolemiso 10550 seq3coll 10553 summodclem2a 11118 |
Copyright terms: Public domain | W3C validator |