Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > f1ofo | Unicode version |
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.) |
Ref | Expression |
---|---|
f1ofo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dff1o3 5373 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 ccnv 4538 wfun 5117 wfo 5121 wf1o 5122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 |
This theorem is referenced by: f1imacnv 5384 f1ococnv2 5394 fo00 5403 isoini 5719 isoselem 5721 f1opw2 5976 f1dmex 6014 bren 6641 f1oeng 6651 en1 6693 mapen 6740 ssenen 6745 phplem4 6749 phplem4on 6761 dif1en 6773 fiintim 6817 fidcenumlemim 6840 supisolem 6895 ordiso2 6920 djuunr 6951 omct 7002 ctssexmid 7024 1fv 9916 hashfacen 10579 fsumf1o 11159 fisumss 11161 ennnfonelemrn 11932 ennnfonelemnn0 11935 ennnfonelemim 11937 exmidunben 11939 ctinfomlemom 11940 ctinfom 11941 qnnen 11944 enctlem 11945 hmeontr 12482 hmeoimaf1o 12483 subctctexmid 13196 exmidsbthrlem 13217 sbthomlem 13220 |
Copyright terms: Public domain | W3C validator |