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 5341 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ◡ccnv 4508 Fun wfun 5087 –onto→wfo 5091 –1-1-onto→wf1o 5092 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-3an 949 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 df-f 5097 df-f1 5098 df-fo 5099 df-f1o 5100 |
This theorem is referenced by: f1imacnv 5352 f1ococnv2 5362 fo00 5371 isoini 5687 isoselem 5689 f1opw2 5944 f1dmex 5982 bren 6609 f1oeng 6619 en1 6661 mapen 6708 ssenen 6713 phplem4 6717 phplem4on 6729 dif1en 6741 fiintim 6785 fidcenumlemim 6808 supisolem 6863 ordiso2 6888 djuunr 6919 omct 6970 ctssexmid 6992 1fv 9884 hashfacen 10547 fsumf1o 11127 fisumss 11129 ennnfonelemrn 11859 ennnfonelemnn0 11862 ennnfonelemim 11864 exmidunben 11866 ctinfomlemom 11867 ctinfom 11868 qnnen 11871 enctlem 11872 hmeontr 12409 hmeoimaf1o 12410 subctctexmid 13123 exmidsbthrlem 13144 sbthomlem 13147 |
Copyright terms: Public domain | W3C validator |