![]() |
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 5294 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) | |
2 | 1 | simplbi 269 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ◡ccnv 4466 Fun wfun 5043 –onto→wfo 5047 –1-1-onto→wf1o 5048 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-in 3019 df-ss 3026 df-f 5053 df-f1 5054 df-fo 5055 df-f1o 5056 |
This theorem is referenced by: f1imacnv 5305 f1ococnv2 5315 fo00 5324 isoini 5635 isoselem 5637 f1opw2 5888 f1dmex 5925 bren 6544 f1oeng 6554 en1 6596 mapen 6642 ssenen 6647 phplem4 6651 phplem4on 6663 dif1en 6675 fiintim 6719 fidcenumlemim 6741 supisolem 6783 ordiso2 6808 djuunr 6838 1fv 9699 hashfacen 10356 fsumf1o 10933 fisumss 10935 exmidsbthrlem 12617 |
Copyright terms: Public domain | W3C validator |