![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1ofo | GIF version |
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.) |
Ref | Expression |
---|---|
f1ofo | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dff1o3 5479 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ◡ccnv 4637 Fun wfun 5222 –onto→wfo 5226 –1-1-onto→wf1o 5227 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-in 3147 df-ss 3154 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 |
This theorem is referenced by: f1imacnv 5490 f1ococnv2 5500 fo00 5509 isoini 5832 isoselem 5834 f1opw2 6091 f1dmex 6131 bren 6761 f1oeng 6771 en1 6813 mapen 6860 ssenen 6865 phplem4 6869 phplem4on 6881 dif1en 6893 fiintim 6942 fidcenumlemim 6965 supisolem 7021 ordiso2 7048 djuunr 7079 omct 7130 ctssexmid 7162 1fv 10153 hashfacen 10830 fsumf1o 11412 fisumss 11414 fprodf1o 11610 fprodssdc 11612 ennnfonelemrn 12434 ennnfonelemnn0 12437 ennnfonelemim 12439 exmidunben 12441 ctinfomlemom 12442 ctinfom 12443 qnnen 12446 enctlem 12447 ssomct 12460 xpsfrn 12788 imasgrpf1 13007 imasrngf1 13209 imasringf1 13313 hmeontr 14109 hmeoimaf1o 14110 subctctexmid 15047 exmidsbthrlem 15067 sbthomlem 15070 |
Copyright terms: Public domain | W3C validator |